Require Import PTS. Require Import Peano_dec. Require Import Compare_dec. Require Import Lt. Require Import Omega. Inductive Beta : Term -> Term -> Prop := | Beta_head : forall A b c, Beta ((λ[ A ], b)· c) ( b [← c]) | Beta_red1 : forall x y z, Beta x y ->Beta (x· z) (y·z) | Beta_red2 : forall x y z, Beta x y -> Beta (z·x) (z · y) | Beta_lam : forall x y A , Beta x y -> Beta (λ [A], x) (λ [ A], y) | Beta_lam2 : forall x A B , Beta A B -> Beta (λ [ A ], x) (λ [B ], x) | Beta_pi : forall x y A ,Beta x y -> Beta (Π (A), x) (Π(A), y) | Beta_pi2 : forall x A B, Beta A B -> Beta (Π(A), x) (Π(B), x) . Notation " A → B " := (Beta A B) (at level 80). Inductive Betas : Term -> Term -> Prop := | Betas_refl : forall x, Betas x x | Betas_Beta : forall x y, x → y -> Betas x y | Betas_trans : forall x y z, Betas x y -> Betas y z -> Betas x z. Notation " A →→ B " := (Betas A B) (at level 80). Inductive Betac : Term -> Term -> Prop := | Betac_Betas : forall x y, x →→ y -> Betac x y | Betac_sym : forall x y, Betac x y -> Betac y x | Betac_trans : forall x y z, Betac x y -> Betac y z -> Betac x z. Notation " A ≡ B " := (Betac A B) (at level 80). Hint Constructors Beta. Hint Constructors Betas. Hint Constructors Betac. (* dummy facts about Betas et Betac, mainly congruence *) Lemma Betac_refl : forall T, T ≡ T. intros; constructor; constructor. Qed. Lemma Betas_App : forall a b c, b →→ c -> a·b →→ a·c. intros; induction H. constructor. constructor; constructor; trivial. apply Betas_trans with (y:= a·y); trivial. Qed. Lemma Betac_App : forall a b c, b ≡ c -> a· b ≡ a· c. intros; induction H. constructor; apply Betas_App; intuition. apply Betac_sym ; intuition. apply Betac_trans with (y:=a· y); intuition. Qed. Lemma Betas_App2: forall a b c, b→→c -> b· a →→ c· a. intros; induction H. constructor. constructor; constructor; trivial. apply Betas_trans with (y:= y· a); trivial. Qed. Lemma Betac_App2 : forall a b c , b ≡ c -> b·a ≡ c·a. intros; induction H. constructor; apply Betas_App2; intuition. apply Betac_sym; intuition. apply Betac_trans with (y:=y·a); intuition. Qed. Lemma Betas_App3 : forall a b c d, a →→ b -> c →→ d -> a·c →→ b·d. intros. apply Betas_trans with (y:= b·c). apply Betas_App2; intuition. apply Betas_App; intuition. Qed. Lemma Betac_App3 : forall a b c d, a ≡ b -> c ≡ d -> a·c ≡ b·d. intros. apply Betac_trans with (y:=b·c). apply Betac_App2; intuition. apply Betac_App; intuition. Qed. Lemma Betas_La : forall a b c , a →→ b -> λ[c], a →→ λ[c], b. intros; induction H. constructor. constructor; constructor; trivial. apply Betas_trans with (y := λ[c], y); trivial. Qed. Lemma Betac_La: forall a b c, a ≡ b -> λ[c], a ≡ λ[c], b. intros. induction H. constructor; apply Betas_La; intuition. apply Betac_sym; intuition. apply Betac_trans with (y:=λ[c],y); intuition. Qed. Lemma Betas_La2: forall a b c, a →→ b -> λ[a], c →→ λ[b], c. intros; induction H. constructor. constructor; constructor; trivial. apply Betas_trans with (y := λ[y], c); trivial. Qed. Lemma Betac_La2: forall a b c, a ≡ b -> λ[a], c ≡ λ[b], c. intros. induction H. constructor; apply Betas_La2; intuition. apply Betac_sym; intuition. apply Betac_trans with (y:=La y c); intuition. Qed. Lemma Betas_La3: forall a b c d, a →→ b -> c →→ d -> λ[a], c →→ λ[b], d. intros. apply Betas_trans with (y := λ[b], c). apply Betas_La2; intuition. apply Betas_La; intuition. Qed. Lemma Betac_La3: forall a b c d, a ≡ b -> c ≡ d -> λ[a],c ≡ λ[b], d. intros. apply Betac_trans with (y := λ[b],c). apply Betac_La2; intuition. apply Betac_La; intuition. Qed. Lemma Betas_Pi : forall a b c , a →→ b -> Π (c), a →→ Π(c), b. intros; induction H. constructor. constructor; constructor; trivial. apply Betas_trans with (y := Π(c),y); trivial. Qed. Lemma Betac_Pi : forall a b c , a ≡ b -> Π(c), a ≡ Π(c), b. intros; induction H. constructor; apply Betas_Pi; intuition. apply Betac_sym; intuition. apply Betac_trans with (y:=Π(c), y); intuition. Qed. Lemma Betas_Pi2: forall a b c, a →→ b -> Π(a), c →→ Π(b), c. intros; induction H. constructor. constructor; constructor; trivial. apply Betas_trans with (y := Π(y), c); trivial. Qed. Lemma Betac_Pi2: forall a b c, a ≡ b -> Π(a), c ≡ Π(b), c. intros; induction H. constructor; apply Betas_Pi2; intuition. apply Betac_sym; intuition. apply Betac_trans with (y:=Π(y), c); intuition. Qed. Lemma Betas_Pi3: forall a b c d, a →→ b -> c →→ d -> Π(a), c →→ Π(b), d. intros. apply Betas_trans with (y := Π(b), c). apply Betas_Pi2; intuition. apply Betas_Pi; intuition. Qed. Lemma Betac_Pi3: forall a b c d, a ≡ b -> c ≡ d -> Π(a), c ≡ Π(b), d. intros. apply Betac_trans with (y := Π(b), c). apply Betac_Pi2; intuition. apply Betac_Pi; intuition. Qed. (* some other facts, not every thing is used in the main development *) Lemma Beta_beta : forall a b c n, a → b -> a[n←c] → b[n←c] . intros. generalize n. induction H; intros. rewrite (subst_travers). simpl. replace (n0+1) with (S n0) by omega. apply Beta_head. simpl ; apply Beta_red1; trivial. simpl ; apply Beta_red2; trivial. simpl ; apply Beta_lam; trivial. simpl ; apply Beta_lam2; trivial. simpl; apply Beta_pi; trivial. simpl; apply Beta_pi2; trivial. Qed. Hint Constructors Betas. Lemma Betas_one_beta : forall a b , a<>b -> a →→ b -> (exists c, a → c /\ c →→ b). intros; induction H0. elim H; reflexivity. exists y; intuition. destruct (eq_term_dec x y). rewrite e in H. destruct (IHBetas2 H). destruct H0. exists x0; split. rewrite e; exact H0. exact H1. destruct (IHBetas1 n). destruct H0. exists x0;split. exact H0. apply Betas_trans with (y:=y); intuition. Qed. Lemma Betas_V_: forall V t, V →→ t -> forall v, V = #v -> t = #v. intros V t H; induction H; intros; try (discriminate). intuition. subst; inversion H. intuition. Qed. Lemma Betas_V : forall v t, #v →→ t -> t = #v. intros; apply Betas_V_ with (V:=#v); intuition. Qed. Lemma Betas_S_: forall S t, S →→ t -> forall s, S = !s -> t = !s. intros S T H; induction H; intros. intuition. subst; inversion H. intuition. Qed. Lemma Betas_S : forall s t, !s →→ t -> t = !s. intros; apply Betas_S_ with !s; intuition. Qed. Lemma Betas_Pi_inv_ : forall s t, s →→ t -> (forall A B, s = Π(A), B -> exists C, exists D , t = Π(C), D /\ A →→ C /\ B →→ D). intros s t H; induction H; intros. exists A; exists B; split; trivial; split; constructor. subst; inversion H; subst. exists A; exists y0; split; trivial; split; constructor; trivial. exists B0; exists B; split; trivial; split; constructor; trivial. subst. destruct (IHBetas1 A B (refl_equal (Π(A), B))) as [ C [ D [ H1 [ H2 H3]]]]. destruct (IHBetas2 C D H1) as [C' [D' [H1' [H2' H3']]]]. exists C'; exists D'; split; trivial; split. apply Betas_trans with (y:=C); trivial. apply Betas_trans with (y:=D); trivial. Qed. Lemma Betas_Pi_inv : forall A B t, Π(A), B →→ t -> exists C, exists D, t = Π(C), D /\ A →→ C /\ B →→ D. intros. apply Betas_Pi_inv_ with (Π(A), B); trivial. Qed. Lemma Betas_La_inv_ : forall s t, s →→ t -> (forall A B, s = λ[A], B -> exists C, exists D , t = λ[C], D /\ A →→ C /\ B →→ D). intros s t H; induction H; intros. exists A; exists B; split; trivial; split; constructor. subst; inversion H; subst. exists A; exists y0; split; trivial; split; constructor; trivial. exists B0; exists B; split; trivial; split; constructor; trivial. subst. destruct (IHBetas1 A B (refl_equal (λ[A], B))) as [ C [ D [ H1 [ H2 H3]]]]. destruct (IHBetas2 C D H1) as [C' [D' [H1' [H2' H3']]]]. exists C'; exists D'; split; trivial; split. apply Betas_trans with (y:=C); trivial. apply Betas_trans with (y:=D); trivial. Qed. Lemma Betas_La_inv : forall A B t, λ[A], B →→ t -> exists C, exists D, t = λ[C], D /\ A →→ C /\ B →→ D. intros. apply Betas_La_inv_ with (λ[A], B); trivial. Qed. (* Beta Betas and Betac are correct related to lift / subst of DeBruijn index *) Lemma Beta_lift: forall a b n m, a → b -> a ↑ n # m → b ↑ n # m . intros. generalize n m; clear n m. induction H; intros. simpl. change m with (0+m). rewrite (substP1 b c m 0 n). apply Beta_head. simpl. constructor; trivial. simpl; constructor; trivial. simpl; constructor; intuition. simpl; constructor; intuition. simpl; constructor; intuition. simpl; constructor; intuition. Qed. Lemma Beta_lift_inv : forall A n m B, A ↑ n # m → B -> exists B', B = B' ↑ n # m /\ A → B'. intros A; induction A; intros; simpl in H. destruct (le_gt_dec m v). inversion H. inversion H. inversion H. inversion H; subst. destruct A1; try discriminate. simpl in H1. destruct (le_gt_dec m v); discriminate. simpl in H1. injection H1; intros. exists (A1_2[← A2]); split. rewrite H0. symmetry. apply (substP1 A1_2 A2 m 0 n). constructor. destruct (IHA1 n m y H3) as [B' [HH HHH]]. exists (B'·A2); subst; intuition. destruct (IHA2 n m y H3) as [B' [HH HHH]]. exists (A1·B'); subst; intuition. simpl in H; inversion H; subst. destruct (IHA2 n (S m) y H3) as [B' [HH HHH]]. exists (Π(A1), B'); subst; intuition. destruct (IHA1 n m B0 H3) as [B' [HH HHH]]. exists (Π(B'), A2); subst; intuition. simpl in H; inversion H; subst. destruct (IHA2 n (S m) y H3) as [B' [HH HHH]]. exists (λ[A1], B'); subst; intuition. destruct (IHA1 n m B0 H3) as [B' [HH HHH]]. exists (λ[B'], A2); subst; intuition. Qed. Lemma Betas_lift : forall a b n m , a →→ b -> a ↑ n # m →→ b ↑ n # m . intros. induction H. constructor. constructor; apply Beta_lift; intuition. apply Betas_trans with (y:= y ↑ n # m ); intuition. Qed. Lemma Betas_lift_inv_: forall A B, A →→ B -> (forall a n m, A=a ↑ n # m -> exists b', B = b' ↑ n # m /\ a →→ b'). intros A B H; induction H; intros. exists a; intuition. rewrite H0 in H; apply Beta_lift_inv in H. destruct H as [B' [H1 H2]]. exists B'; intuition. destruct (IHBetas1 a n m H1) as [B1 [H'1 H'2]]. destruct (IHBetas2 B1 n m H'1) as [B' [K L]]. exists B'; intuition. apply Betas_trans with (y:=B1); intuition. Qed. Lemma Betas_lift_inv : forall a b n m, a ↑ n # m →→ b -> exists b', b = b' ↑ n # m /\ a →→ b'. intros; apply Betas_lift_inv_ with (a ↑ n # m); trivial. Qed. Lemma Betac_lift : forall a b n m, a ≡ b -> a ↑ n # m ≡ b ↑ n # m . intros. induction H. constructor. apply Betas_lift; trivial. apply Betac_sym; trivial. apply Betac_trans with (y:=y ↑ n # m); trivial. Qed. Lemma Betas_subst : forall c a b n, a →→ b -> c [n←a] →→ c[n← b]. intros c. induction c; intros. simpl. destruct (lt_eq_lt_dec v n). destruct s. constructor. apply Betas_lift; intuition. constructor. simpl; constructor. simpl. apply Betas_App3; intuition. simpl. apply Betas_Pi3; intuition. simpl; apply Betas_La3; intuition. Qed. Lemma Betas_subst2 : forall c a b n, a →→ b -> a [n← c] →→ b [n ← c]. intros. induction H. constructor. constructor. apply Beta_beta; intuition. apply Betas_trans with (y:= y[n←c]); intuition. Qed. Lemma Betac_subst : forall c a b n, a ≡ b -> c[n←a] ≡ c [n←b]. intros c. induction c; intros. simpl. destruct (lt_eq_lt_dec v n). destruct s. apply Betac_refl. apply Betac_lift; intuition. apply Betac_refl. simpl; apply Betac_refl. simpl. apply Betac_App3; intuition. simpl. apply Betac_Pi3; intuition. simpl. apply Betac_La3; intuition. Qed. Lemma Betac_subst2 : forall c a b n, a ≡ b -> a[n←c] ≡ b[n← c] . intros. induction H. constructor; apply Betas_subst2; intuition. apply Betac_sym; intuition. apply Betac_trans with (y:= y[n←c]); intuition. Qed. (* Beta parallel definition *) Inductive Betap : Term -> Term -> Prop := | Betap_refl : forall m, Betap m m | Betap_lam: forall m m' A A', Betap m m' ->Betap A A'-> Betap (λ [ A], m) (λ[ A'], m') | Betap_pi: forall m m' A A', Betap m m' -> Betap A A' -> Betap (Π(A), m) (Π(A'), m') | Betap_App : forall m m' n n', Betap m m' -> Betap n n' -> Betap (m·n) (m'·n') | Betap_head : forall m m' n n' A, Betap m m' -> Betap n n' -> Betap((λ[A], m)· n) (m'[← n']). Notation "m →' n" := (Betap m n) (at level 80). Lemma Betap_lift: forall a b n m, a →' b -> a ↑ n # m →' b ↑ n # m . intros. generalize n m; clear n m. induction H; intros. constructor. simpl; constructor . apply IHBetap1; intuition. apply IHBetap2; intuition. simpl; constructor . apply IHBetap1; intuition. apply IHBetap2; intuition. simpl; constructor . apply IHBetap1; intuition. apply IHBetap2; intuition. simpl. change m0 with (0+m0). rewrite substP1. constructor. apply IHBetap1. apply IHBetap2. Qed. (* inversion lemmas for beta // *) Lemma Betap1:forall m m' n n' x, m →' m' -> n →' n' -> m[x←n] →' m'[x←n']. intros. generalize x; clear x. induction H. (* 1/5 *) induction m;intros; simpl. destruct (lt_eq_lt_dec v x). destruct s. constructor. apply Betap_lift; trivial. constructor. constructor. constructor; trivial. constructor; trivial. constructor; trivial. (* 2/5 *) intros; simpl ; constructor. apply IHBetap1; intuition. apply IHBetap2; intuition. (* 3/5 *) intros; simpl ; constructor. apply IHBetap1; intuition. apply IHBetap2; intuition. (* 4/5 *) intros; simpl ; constructor. apply IHBetap1; intuition. apply IHBetap2; intuition. (* 5/5 *) intros; simpl . assert ( (m' [x+1 ← n']) [← n'0[x←n']] = (m'[← n'0])[x← n'] ). symmetry. apply subst_travers. rewrite <- H2. replace (S x) with (x+1) by omega; constructor; intuition. Qed. Lemma Betap2 : forall m n A, (λ[A], m) →' n -> (exists m', exists A', (n = (λ[A'], m')) /\ m →' m' /\ A →' A'). intros. inversion H; subst. exists m; exists A; split; intuition . constructor. constructor. exists m'; exists A'; split. intuition. split; trivial. Qed. Lemma Betap2' : forall m n A, (Π(A), m) →' n -> (exists m', exists A', (n = (Π(A'), m')) /\ m →' m' /\ A →' A'). intros. inversion H; subst. exists m; exists A; split; intuition . constructor. constructor. exists m'; exists A'; split. intuition. split; trivial. Qed. Lemma Betap3 : forall m n l, (m·n) →' l -> ( exists m', exists n', l = m'·n' /\ m →' m' /\ n →' n') \/ ( exists p, exists p', exists n',exists A, m = λ[A], p /\ l = p'[← n'] /\ p →' p'/\ n →' n'). intros. inversion H; subst. left. exists m; exists n; split. intuition. split; constructor. left. exists m'; exists n'; split ; intuition. right. exists m0; exists m'; exists n'; exists A. split; intuition. Qed. (* Beta // has the diamond property *) Lemma Betap_diamond : forall m m1 m2 , m →' m1 -> m →' m2 -> (exists m3, m1 →' m3 /\ m2 →' m3). intros. generalize m2 H0; clear m2 H0. induction H; intros. (*1/5*) exists m2; intuition. constructor. (*2/5*) destruct (Betap2 m m2 A H1). destruct H2. destruct H2. destruct H3. subst. destruct (IHBetap1 x H3). destruct H2. destruct (IHBetap2 x0 H4). destruct H6. exists (λ[x2], x1); split; constructor; intuition. (*3/5*) destruct (Betap2' m m2 A H1). destruct H2; destruct H2; destruct H3; subst. destruct (IHBetap1 x H3); destruct H2. destruct (IHBetap2 x0 H4); destruct H6. exists (Π(x2), x1); split; constructor; intuition. (*4/5*) destruct (Betap3 m n m2 H1). destruct H2; destruct H2; destruct H2. destruct H3. subst. destruct (IHBetap1 x H3). destruct H2. destruct (IHBetap2 x0 H4). destruct H6. exists (x1·x2); split; constructor; intuition. destruct H2; destruct H2; destruct H2; destruct H2. destruct H2. destruct H3. destruct H4. subst. destruct (Betap2 x m' x2); intuition. destruct H2; destruct H2; destruct H3; subst. destruct (IHBetap2 x1 H5). destruct H2. destruct (IHBetap1 (λ[x2], x0)). constructor; intuition; constructor. destruct H8. destruct (Betap2 x3 x6 x4 H8). destruct H10; destruct H10. destruct H11; subst. exists ( x7[← x5] ) ;split. constructor; intuition. apply Betap1; intuition. inversion H9. constructor. subst. trivial. (*5/5*) destruct (Betap3 (λ[A], m) n m2 H1). destruct H2; destruct H2. destruct H2; destruct H3. subst. destruct (Betap2 m x A H3). destruct H2; destruct H2; destruct H5. subst. destruct (IHBetap1 x1 H5). destruct H2. destruct (IHBetap2 x0 H4). destruct H8. exists (x[← x3]); split. apply Betap1. exact H2. exact H8. constructor. exact H7. exact H9. destruct H2; destruct H2; destruct H2; destruct H2. destruct H2; destruct H3; destruct H4. subst. inversion H2; subst; clear H2. destruct (IHBetap1 x0 H4). destruct H2. destruct (IHBetap2 x1 H5). destruct H6. exists (x3[← x4]); split. apply Betap1; intuition. apply Betap1; intuition. Qed. Inductive Betaps : Term -> Term -> Prop := | Betaps_refl : forall x , Betaps x x | Betaps_trans : forall x y z , Betap x y -> Betaps y z -> Betaps x z . Notation " x →→' y " := (Betaps x y) (at level 80). (* the closure of Beta is the same as Beta // *) Lemma Betas_Betap_closure : forall x y , x →' y -> x →→ y. intros. induction H. constructor. apply Betas_La3; intuition. apply Betas_Pi3; intuition. apply Betas_App3; intuition. apply Betas_trans with (y:= (λ[A], m')· n). apply Betas_App2; intuition. apply Betas_La; intuition. apply Betas_trans with (y:= (λ[A], m')· n'). apply Betas_App; intuition. constructor; constructor. Qed. Lemma Betas_Betaps_closure : forall x y , x →→' y -> x →→ y. intros. induction H. constructor. apply Betas_trans with (y:= y); trivial. apply Betas_Betap_closure; intuition. Qed. Lemma Betap_Beta_closure : forall x y, x → y -> x →' y. intros. induction H; constructor; intuition; constructor. Qed. Lemma Betaps_Beta_closure :forall x y, x → y -> x →→' y. intros. apply Betaps_trans with (y:=y). apply Betap_Beta_closure; intuition. constructor. Qed. Lemma Betaps_trans2 : forall x y z , x →→' y -> y →→' z -> x →→' z. intros. generalize z H0; clear z H0. induction H; intros. intuition. apply Betaps_trans with (y:=y). exact H. apply IHBetaps; intuition. Qed. Lemma Betaps_Betas_closure : forall x y , x →→ y -> x →→' y. intros. induction H. constructor. apply Betaps_Beta_closure ; intuition. apply Betaps_trans2 with (y:= y); intuition. Qed. Lemma sub_diamond_Betaps : ( forall x y z, x →' y -> x →' z -> (exists t, y →' t /\ z →' t) ) -> forall x y z , x →' y -> x →→' z ->(exists t, y →→' t /\ z →' t). intros. generalize y H0; clear y H0. induction H1; intros. exists y; split . constructor. intuition. destruct (H x y y0 H0 H2). destruct H3. destruct (IHBetaps x0 H3). destruct H5. exists x1; split. apply Betaps_trans with (y:=x0); intuition. intuition. Qed. Lemma diamond_Betaps : ( forall x y z, x →' y -> x →' z -> (exists t, y →' t /\ z →' t) ) -> forall x y z, x →→' y -> x →→' z -> (exists t,y →→' t /\ z →→' t) . intros. generalize z H1; clear z H1. induction H0; intros. exists z; split. intuition. constructor. destruct (sub_diamond_Betaps H x y z0 H0 H2). destruct H3. destruct (IHBetaps x0 H3). destruct H5. exists x1; split. intuition. apply Betaps_trans with (y:= x0); intuition. Qed. (* from all this => Beta* is confluent \o/ a hand written proof is in Barendregt *) Lemma Betas_diamond: forall x y z, x →→ y -> x →→ z -> (exists t, y →→ t /\ z →→ t). intros. destruct (diamond_Betaps Betap_diamond x y z). apply Betaps_Betas_closure; intuition. apply Betaps_Betas_closure; intuition. destruct H1. exists x0; split. apply Betas_Betaps_closure; intuition. apply Betas_Betaps_closure; intuition. Qed. (* facts about confluency & church rosser *) Lemma Betac_confl : forall x y, x ≡ y -> (exists z, x →→ z /\ y →→ z). intros. induction H. exists y; split; trivial. destruct IHBetac as [z [H1 H2]]. exists z; split; trivial. destruct IHBetac1 as [z1 [H1 H2]]. destruct IHBetac2 as [z2 [H3 H4]]. destruct (Betas_diamond y z1 z2 H2 H3) as [z0 [K L]]. exists z0; split . apply Betas_trans with (y:=z1); trivial. apply Betas_trans with (y:=z2); trivial. Qed. Lemma conv_sort : forall s t, !s ≡ !t -> s = t. intros. apply Betac_confl in H. destruct H as [z [K L]]. apply Betas_S in K. apply Betas_S in L. rewrite K in L. injection L; trivial. Qed. Lemma conv_to_sort : forall s T, !s ≡ T -> T →→ !s. intros. apply Betac_confl in H. destruct H as [z [K L]]. apply Betas_S in K. subst. trivial. Qed. Lemma conv_to_var : forall v T , #v ≡ T -> T →→ #v. intros. apply Betac_confl in H. destruct H as [z [K L]]. apply Betas_V in K. subst; trivial. Qed. Lemma Betac_V : forall s t, #s ≡ #t -> s = t. intros. apply conv_to_var in H. apply Betas_V in H. injection H; trivial. Qed. (* Pi is injective *) Lemma Betac_Pi_inv : forall A B C D, Π(A), B ≡ Π(C), D -> A ≡ C /\ B ≡ D. intros. apply Betac_confl in H. destruct H as [z [h1 h2]]. apply Betas_Pi_inv in h1. apply Betas_Pi_inv in h2. destruct h1 as [c1 [d1 [a [b c]]]]. destruct h2 as [c2 [d2 [e [f g]]]]. rewrite a in e; injection e; intros; subst. split. apply Betac_trans with (y:=c2). constructor; trivial. apply Betac_sym; constructor; trivial. apply Betac_trans with (y:=d2). constructor; trivial. apply Betac_sym; constructor; trivial. Qed.