Library ut_red








Beta-reduction definition and properties.







Require Import base ut_term.



Require Import Peano_dec.



Require Import Compare_dec.



Require Import Lt Plus.






Module Type ut_red_mod (X:term_sig)  (TM : ut_term_mod X).
Interactive Module Type ut_red_mod started





 Import TM.














Usual Beta-reduction:





 



    

  •  one step


    • 

  •  multi step (reflexive, transitive closure)


    • 

  •  converesion (reflexive, symetric, transitive closure)


    • 


 





Reserved Notation " A → B " (at level 80).






Inductive Beta : Term -> Term -> Prop :=

 | Beta_head : forall A M  N , (λ[A], M)· N → M [← N]

 | Beta_red1 : forall M M' N , M → M' -> M · N  → M'· N

 | Beta_red2 : forall M N  N', N → N' -> M · N  → M · N'

 | Beta_lam  : forall A M  M', M → M' -> λ[A],M → λ[A ],M'

 | Beta_lam2 : forall A A' M , A → A' -> λ[A],M → λ[A'],M

 | Beta_pi   : forall A B  B', B → B' -> Π(A),B → Π(A ),B'

 | Beta_pi2  : forall A A' B , A → A' -> Π(A),B → Π(A'),B

where "M → N" := (Beta M N) : UT_scope.
Beta is defined
Beta_ind is defined








Reserved Notation " A →→ B " (at level 80).






Inductive Betas : Term -> Term -> Prop :=

 | Betas_refl  : forall M    , M →→ M

 | Betas_Beta  : forall M N  , M → N  -> M →→ N

 | Betas_trans : forall M N P, M →→ N -> N →→ P -> M →→ P

where  " A →→ B " := (Betas A B) : UT_scope.
Betas is defined
Betas_ind is defined








Reserved Notation " A ≡ B " (at level 80).






Inductive Betac : Term -> Term -> Prop :=

 | Betac_Betas : forall M N  , M →→ N -> M ≡ N

 | Betac_sym   : forall M N  , M ≡ N  -> N ≡ M

 | Betac_trans : forall M N P, M ≡ N   -> N ≡ P -> M ≡ P

where " A ≡ B " := (Betac A B)  : UT_scope.
Betac is defined
Betac_ind is defined








Hint Constructors Beta.



Hint Constructors Betas.
Warning: the hint: eapply Betas_trans will only be used by eauto





Hint Constructors Betac.
Warning: the hint: eapply Betac_trans will only be used by eauto















Facts about Betas and Betac: Congruence. 





Lemma Betac_refl : forall M, M ≡ M.
1 subgoals, subgoal 1 (ID 36)
  
  ============================
   forall M : Term, M ≡ M

(dependent evars:)





intros; constructor; constructor.
No more subgoals.
(dependent evars:)





Qed.
Betac_refl is defined








Hint Resolve Betac_refl.






Lemma Betas_App : forall M M' N N',M →→ M' -> N →→ N' -> M · N →→ M' · N'.
1 subgoals, subgoal 1 (ID 45)
  
  ============================
   forall M M' N N' : Term, M →→ M' -> N →→ N' -> M · N →→ M' · N'

(dependent evars:)





assert (forall a b c, b →→ c ->  a·b →→ a·c).
2 subgoals, subgoal 1 (ID 49)
  
  ============================
   forall a b c : Term, b →→ c -> a · b →→ a · c

subgoal 2 (ID 50) is:
 forall M M' N N' : Term, M →→ M' -> N →→ N' -> M · N →→ M' · N'
(dependent evars:)





induction 1; eauto.
1 subgoals, subgoal 1 (ID 50)
  
  H : forall a b c : Term, b →→ c -> a · b →→ a · c
  ============================
   forall M M' N N' : Term, M →→ M' -> N →→ N' -> M · N →→ M' · N'

(dependent evars: ?89 using ,)





assert (forall a b c, b→→c -> b· a →→ c· a).
2 subgoals, subgoal 1 (ID 104)
  
  H : forall a b c : Term, b →→ c -> a · b →→ a · c
  ============================
   forall a b c : Term, b →→ c -> b · a →→ c · a

subgoal 2 (ID 105) is:
 forall M M' N N' : Term, M →→ M' -> N →→ N' -> M · N →→ M' · N'
(dependent evars: ?89 using ,)





induction 1; eauto.
1 subgoals, subgoal 1 (ID 105)
  
  H : forall a b c : Term, b →→ c -> a · b →→ a · c
  H0 : forall a b c : Term, b →→ c -> b · a →→ c · a
  ============================
   forall M M' N N' : Term, M →→ M' -> N →→ N' -> M · N →→ M' · N'

(dependent evars: ?89 using , ?145 using ,)





intros; eauto.
No more subgoals.
(dependent evars: ?89 using , ?145 using , ?167 using , ?181 using ?185 ?184 , ?184 using , ?185 using ,)





Qed.
Betas_App is defined








Hint Resolve Betas_App.






Lemma Betac_App : forall M M' N N' , M ≡ M' -> N ≡ N' -> M · N ≡ M' · N'.
1 subgoals, subgoal 1 (ID 299)
  
  ============================
   forall M M' N N' : Term, M ≡ M' -> N ≡ N' -> M · N ≡ M' · N'

(dependent evars:)





assert (forall a b c, b ≡ c ->  a· b ≡ a· c).
2 subgoals, subgoal 1 (ID 303)
  
  ============================
   forall a b c : Term, b ≡ c -> a · b ≡ a · c

subgoal 2 (ID 304) is:
 forall M M' N N' : Term, M ≡ M' -> N ≡ N' -> M · N ≡ M' · N'
(dependent evars:)





induction 1; eauto.
1 subgoals, subgoal 1 (ID 304)
  
  H : forall a b c : Term, b ≡ c -> a · b ≡ a · c
  ============================
   forall M M' N N' : Term, M ≡ M' -> N ≡ N' -> M · N ≡ M' · N'

(dependent evars: ?414 using ,)





assert (forall a b c , b ≡ c -> b·a ≡ c·a).
2 subgoals, subgoal 1 (ID 485)
  
  H : forall a b c : Term, b ≡ c -> a · b ≡ a · c
  ============================
   forall a b c : Term, b ≡ c -> b · a ≡ c · a

subgoal 2 (ID 486) is:
 forall M M' N N' : Term, M ≡ M' -> N ≡ N' -> M · N ≡ M' · N'
(dependent evars: ?414 using ,)





induction 1; eauto.
1 subgoals, subgoal 1 (ID 486)
  
  H : forall a b c : Term, b ≡ c -> a · b ≡ a · c
  H0 : forall a b c : Term, b ≡ c -> b · a ≡ c · a
  ============================
   forall M M' N N' : Term, M ≡ M' -> N ≡ N' -> M · N ≡ M' · N'

(dependent evars: ?414 using , ?599 using ,)





eauto.
No more subgoals.
(dependent evars: ?414 using , ?599 using , ?677 using , ?2161 using ?2437 ?2436 , ?2436 using , ?2437 using ,)





Qed.
Betac_App is defined








Hint Resolve Betac_App.






Lemma Betas_La : forall A A' M M', A →→ A' -> M →→ M' -> λ[A],M →→ λ[A'],M'.
1 subgoals, subgoal 1 (ID 2659)
  
  ============================
   forall A A' M M' : Term, A →→ A' -> M →→ M' -> λ [A], M →→ λ [A'], M'

(dependent evars:)





assert (forall a b c , a →→ b -> λ[c],  a →→ λ[c], b).
2 subgoals, subgoal 1 (ID 2663)
  
  ============================
   forall a b c : Term, a →→ b -> λ [c], a →→ λ [c], b

subgoal 2 (ID 2664) is:
 forall A A' M M' : Term, A →→ A' -> M →→ M' -> λ [A], M →→ λ [A'], M'
(dependent evars:)





induction 1; eauto.
1 subgoals, subgoal 1 (ID 2664)
  
  H : forall a b c : Term, a →→ b -> λ [c], a →→ λ [c], b
  ============================
   forall A A' M M' : Term, A →→ A' -> M →→ M' -> λ [A], M →→ λ [A'], M'

(dependent evars: ?2703 using ,)





assert (forall a b c, a →→ b -> λ[a], c →→ λ[b], c).
2 subgoals, subgoal 1 (ID 2718)
  
  H : forall a b c : Term, a →→ b -> λ [c], a →→ λ [c], b
  ============================
   forall a b c : Term, a →→ b -> λ [a], c →→ λ [b], c

subgoal 2 (ID 2719) is:
 forall A A' M M' : Term, A →→ A' -> M →→ M' -> λ [A], M →→ λ [A'], M'
(dependent evars: ?2703 using ,)





induction 1; eauto.
1 subgoals, subgoal 1 (ID 2719)
  
  H : forall a b c : Term, a →→ b -> λ [c], a →→ λ [c], b
  H0 : forall a b c : Term, a →→ b -> λ [a], c →→ λ [b], c
  ============================
   forall A A' M M' : Term, A →→ A' -> M →→ M' -> λ [A], M →→ λ [A'], M'

(dependent evars: ?2703 using , ?2759 using ,)





eauto.
No more subgoals.
(dependent evars: ?2703 using , ?2759 using , ?2781 using , ?2795 using ?2799 ?2798 , ?2798 using , ?2799 using ,)





Qed.
Betas_La is defined








Hint Resolve Betas_La.






Lemma Betac_La: forall A A' M M', A ≡ A' -> M ≡ M' -> λ[A],M ≡ λ[A'],M'.
1 subgoals, subgoal 1 (ID 2913)
  
  ============================
   forall A A' M M' : Term, A ≡ A' -> M ≡ M' -> λ [A], M ≡ λ [A'], M'

(dependent evars:)





assert (forall a b c, a ≡ b -> λ[c], a ≡ λ[c], b).
2 subgoals, subgoal 1 (ID 2917)
  
  ============================
   forall a b c : Term, a ≡ b -> λ [c], a ≡ λ [c], b

subgoal 2 (ID 2918) is:
 forall A A' M M' : Term, A ≡ A' -> M ≡ M' -> λ [A], M ≡ λ [A'], M'
(dependent evars:)





induction 1; eauto.
1 subgoals, subgoal 1 (ID 2918)
  
  H : forall a b c : Term, a ≡ b -> λ [c], a ≡ λ [c], b
  ============================
   forall A A' M M' : Term, A ≡ A' -> M ≡ M' -> λ [A], M ≡ λ [A'], M'

(dependent evars: ?3028 using ,)





assert (forall a b c, a ≡ b -> λ[a], c ≡ λ[b], c).
2 subgoals, subgoal 1 (ID 3099)
  
  H : forall a b c : Term, a ≡ b -> λ [c], a ≡ λ [c], b
  ============================
   forall a b c : Term, a ≡ b -> λ [a], c ≡ λ [b], c

subgoal 2 (ID 3100) is:
 forall A A' M M' : Term, A ≡ A' -> M ≡ M' -> λ [A], M ≡ λ [A'], M'
(dependent evars: ?3028 using ,)





induction 1; eauto.
1 subgoals, subgoal 1 (ID 3100)
  
  H : forall a b c : Term, a ≡ b -> λ [c], a ≡ λ [c], b
  H0 : forall a b c : Term, a ≡ b -> λ [a], c ≡ λ [b], c
  ============================
   forall A A' M M' : Term, A ≡ A' -> M ≡ M' -> λ [A], M ≡ λ [A'], M'

(dependent evars: ?3028 using , ?3213 using ,)





eauto.
No more subgoals.
(dependent evars: ?3028 using , ?3213 using , ?3291 using , ?4781 using ?5057 ?5056 , ?5056 using , ?5057 using ,)





Qed.
Betac_La is defined








Hint Resolve Betac_La.






Lemma Betas_Pi : forall A A' B B', A →→ A' -> B →→ B' -> Π(A),B →→ Π(A'),B'.
1 subgoals, subgoal 1 (ID 5279)
  
  ============================
   forall A A' B B' : Term, A →→ A' -> B →→ B' -> Π (A), B →→ Π (A'), B'

(dependent evars:)





assert (forall a b c , a →→ b -> Π (c), a →→ Π(c), b).
2 subgoals, subgoal 1 (ID 5283)
  
  ============================
   forall a b c : Term, a →→ b -> Π (c), a →→ Π (c), b

subgoal 2 (ID 5284) is:
 forall A A' B B' : Term, A →→ A' -> B →→ B' -> Π (A), B →→ Π (A'), B'
(dependent evars:)





induction 1; eauto.
1 subgoals, subgoal 1 (ID 5284)
  
  H : forall a b c : Term, a →→ b -> Π (c), a →→ Π (c), b
  ============================
   forall A A' B B' : Term, A →→ A' -> B →→ B' -> Π (A), B →→ Π (A'), B'

(dependent evars: ?5323 using ,)





assert (forall a b c, a →→ b -> Π(a), c →→ Π(b), c).
2 subgoals, subgoal 1 (ID 5338)
  
  H : forall a b c : Term, a →→ b -> Π (c), a →→ Π (c), b
  ============================
   forall a b c : Term, a →→ b -> Π (a), c →→ Π (b), c

subgoal 2 (ID 5339) is:
 forall A A' B B' : Term, A →→ A' -> B →→ B' -> Π (A), B →→ Π (A'), B'
(dependent evars: ?5323 using ,)





induction 1; eauto.
1 subgoals, subgoal 1 (ID 5339)
  
  H : forall a b c : Term, a →→ b -> Π (c), a →→ Π (c), b
  H0 : forall a b c : Term, a →→ b -> Π (a), c →→ Π (b), c
  ============================
   forall A A' B B' : Term, A →→ A' -> B →→ B' -> Π (A), B →→ Π (A'), B'

(dependent evars: ?5323 using , ?5379 using ,)





eauto.
No more subgoals.
(dependent evars: ?5323 using , ?5379 using , ?5401 using , ?5415 using ?5419 ?5418 , ?5418 using , ?5419 using ,)





Qed.
Betas_Pi is defined








Hint Resolve Betas_Pi.






Lemma Betac_Pi : forall A A' B B', A ≡ A' -> B ≡ B' -> Π(A),B ≡ Π(A'),B'.
1 subgoals, subgoal 1 (ID 5533)
  
  ============================
   forall A A' B B' : Term, A ≡ A' -> B ≡ B' -> Π (A), B ≡ Π (A'), B'

(dependent evars:)





assert (forall a b c , a ≡ b -> Π(c), a ≡ Π(c), b).
2 subgoals, subgoal 1 (ID 5537)
  
  ============================
   forall a b c : Term, a ≡ b -> Π (c), a ≡ Π (c), b

subgoal 2 (ID 5538) is:
 forall A A' B B' : Term, A ≡ A' -> B ≡ B' -> Π (A), B ≡ Π (A'), B'
(dependent evars:)





induction 1; eauto.
1 subgoals, subgoal 1 (ID 5538)
  
  H : forall a b c : Term, a ≡ b -> Π (c), a ≡ Π (c), b
  ============================
   forall A A' B B' : Term, A ≡ A' -> B ≡ B' -> Π (A), B ≡ Π (A'), B'

(dependent evars: ?5648 using ,)





assert (forall a b c, a ≡ b -> Π(a), c ≡ Π(b), c).
2 subgoals, subgoal 1 (ID 5719)
  
  H : forall a b c : Term, a ≡ b -> Π (c), a ≡ Π (c), b
  ============================
   forall a b c : Term, a ≡ b -> Π (a), c ≡ Π (b), c

subgoal 2 (ID 5720) is:
 forall A A' B B' : Term, A ≡ A' -> B ≡ B' -> Π (A), B ≡ Π (A'), B'
(dependent evars: ?5648 using ,)





induction 1; eauto.
1 subgoals, subgoal 1 (ID 5720)
  
  H : forall a b c : Term, a ≡ b -> Π (c), a ≡ Π (c), b
  H0 : forall a b c : Term, a ≡ b -> Π (a), c ≡ Π (b), c
  ============================
   forall A A' B B' : Term, A ≡ A' -> B ≡ B' -> Π (A), B ≡ Π (A'), B'

(dependent evars: ?5648 using , ?5833 using ,)





eauto.
No more subgoals.
(dependent evars: ?5648 using , ?5833 using , ?5911 using , ?7407 using ?7683 ?7682 , ?7682 using , ?7683 using ,)





Qed.
Betac_Pi is defined








Hint Resolve Betac_Pi.






Lemma Beta_beta : forall M N P n,  M → N ->  M[n←P] → N[n←P] .
1 subgoals, subgoal 1 (ID 7905)
  
  ============================
   forall (M N P : Term) (n : nat), M → N -> M [n ← P] → N [n ← P]

(dependent evars:)





intros.
1 subgoals, subgoal 1 (ID 7910)
  
  M : Term
  N : Term
  P : Term
  n : nat
  H : M → N
  ============================
   M [n ← P] → N [n ← P]

(dependent evars:)





generalize n.
1 subgoals, subgoal 1 (ID 7911)
  
  M : Term
  N : Term
  P : Term
  n : nat
  H : M → N
  ============================
   forall n0 : nat, M [n0 ← P] → N [n0 ← P]

(dependent evars:)





induction H; intros; simpl; intuition.
1 subgoals, subgoal 1 (ID 7980)
  
  P : Term
  n : nat
  A : Term
  M : Term
  N : Term
  n0 : nat
  ============================
   (λ [A [n0 ← P]], M [(S n0) ← P]) · N [n0 ← P] → M [ ← N] [n0 ← P]

(dependent evars:)





rewrite (subst_travers).
1 subgoals, subgoal 1 (ID 8054)
  
  P : Term
  n : nat
  A : Term
  M : Term
  N : Term
  n0 : nat
  ============================
   (λ [A [n0 ← P]], M [(S n0) ← P]) · N [n0 ← P]
   → (M [(n0 + 1) ← P]) [ ← N [n0 ← P]]

(dependent evars:)





replace (n0+1) with (S n0).
2 subgoals, subgoal 1 (ID 8058)
  
  P : Term
  n : nat
  A : Term
  M : Term
  N : Term
  n0 : nat
  ============================
   (λ [A [n0 ← P]], M [(S n0) ← P]) · N [n0 ← P]
   → (M [(S n0) ← P]) [ ← N [n0 ← P]]

subgoal 2 (ID 8055) is:
 S n0 = n0 + 1
(dependent evars:)





constructor.
1 subgoals, subgoal 1 (ID 8055)
  
  P : Term
  n : nat
  A : Term
  M : Term
  N : Term
  n0 : nat
  ============================
   S n0 = n0 + 1

(dependent evars:)





rewrite plus_comm. 
1 subgoals, subgoal 1 (ID 8061)
  
  P : Term
  n : nat
  A : Term
  M : Term
  N : Term
  n0 : nat
  ============================
   S n0 = 1 + n0

(dependent evars:)



trivial.
No more subgoals.
(dependent evars:)





Qed.
Beta_beta is defined















Some "inversion" lemmas : 


 



    

  •  a variable/sort cannot reduce at all


    • 

  •  a pi/lam can only reduce to another pi/lam


    • 

  •  ...


    • 








Lemma Betas_V : forall x N, #x →→ N -> N = #x.
1 subgoals, subgoal 1 (ID 8065)
  
  ============================
   forall (x : Vars) (N : Term), #x →→ N -> N = #x

(dependent evars:)





intros. 
1 subgoals, subgoal 1 (ID 8068)
  
  x : Vars
  N : Term
  H : #x →→ N
  ============================
   N = #x

(dependent evars:)



remember #x as X; induction H; trivial.
2 subgoals, subgoal 1 (ID 8097)
  
  x : Vars
  M : Term
  HeqX : M = #x
  N : Term
  H : M → N
  ============================
   N = M

subgoal 2 (ID 8107) is:
 P = M
(dependent evars:)





subst; inversion H.
1 subgoals, subgoal 1 (ID 8107)
  
  x : Vars
  M : Term
  HeqX : M = #x
  N : Term
  P : Term
  H : M →→ N
  H0 : N →→ P
  IHBetas1 : M = #x -> N = M
  IHBetas2 : N = #x -> P = N
  ============================
   P = M

(dependent evars:)





transitivity N. 
2 subgoals, subgoal 1 (ID 8236)
  
  x : Vars
  M : Term
  HeqX : M = #x
  N : Term
  P : Term
  H : M →→ N
  H0 : N →→ P
  IHBetas1 : M = #x -> N = M
  IHBetas2 : N = #x -> P = N
  ============================
   P = N

subgoal 2 (ID 8237) is:
 N = M
(dependent evars:)



apply IHBetas2. 
2 subgoals, subgoal 1 (ID 8238)
  
  x : Vars
  M : Term
  HeqX : M = #x
  N : Term
  P : Term
  H : M →→ N
  H0 : N →→ P
  IHBetas1 : M = #x -> N = M
  IHBetas2 : N = #x -> P = N
  ============================
   N = #x

subgoal 2 (ID 8237) is:
 N = M
(dependent evars:)



rewrite <- HeqX; intuition. 
1 subgoals, subgoal 1 (ID 8237)
  
  x : Vars
  M : Term
  HeqX : M = #x
  N : Term
  P : Term
  H : M →→ N
  H0 : N →→ P
  IHBetas1 : M = #x -> N = M
  IHBetas2 : N = #x -> P = N
  ============================
   N = M

(dependent evars:)



intuition.
No more subgoals.
(dependent evars:)





Qed.
Betas_V is defined








Lemma Betas_S : forall s N, !s →→ N -> N = !s.
1 subgoals, subgoal 1 (ID 8273)
  
  ============================
   forall (s : X.Sorts) (N : Term), !s →→ N -> N = !s

(dependent evars:)





intros. 
1 subgoals, subgoal 1 (ID 8276)
  
  s : X.Sorts
  N : Term
  H : !s →→ N
  ============================
   N = !s

(dependent evars:)



remember !s as S; induction H; trivial.
2 subgoals, subgoal 1 (ID 8305)
  
  s : X.Sorts
  M : Term
  HeqS : M = !s
  N : Term
  H : M → N
  ============================
   N = M

subgoal 2 (ID 8315) is:
 P = M
(dependent evars:)





subst; inversion H.
1 subgoals, subgoal 1 (ID 8315)
  
  s : X.Sorts
  M : Term
  HeqS : M = !s
  N : Term
  P : Term
  H : M →→ N
  H0 : N →→ P
  IHBetas1 : M = !s -> N = M
  IHBetas2 : N = !s -> P = N
  ============================
   P = M

(dependent evars:)





transitivity N. 
2 subgoals, subgoal 1 (ID 8444)
  
  s : X.Sorts
  M : Term
  HeqS : M = !s
  N : Term
  P : Term
  H : M →→ N
  H0 : N →→ P
  IHBetas1 : M = !s -> N = M
  IHBetas2 : N = !s -> P = N
  ============================
   P = N

subgoal 2 (ID 8445) is:
 N = M
(dependent evars:)



apply IHBetas2. 
2 subgoals, subgoal 1 (ID 8446)
  
  s : X.Sorts
  M : Term
  HeqS : M = !s
  N : Term
  P : Term
  H : M →→ N
  H0 : N →→ P
  IHBetas1 : M = !s -> N = M
  IHBetas2 : N = !s -> P = N
  ============================
   N = !s

subgoal 2 (ID 8445) is:
 N = M
(dependent evars:)



rewrite <- HeqS; intuition. 
1 subgoals, subgoal 1 (ID 8445)
  
  s : X.Sorts
  M : Term
  HeqS : M = !s
  N : Term
  P : Term
  H : M →→ N
  H0 : N →→ P
  IHBetas1 : M = !s -> N = M
  IHBetas2 : N = !s -> P = N
  ============================
   N = M

(dependent evars:)



intuition.
No more subgoals.
(dependent evars:)





Qed.
Betas_S is defined








Lemma Betas_Pi_inv : forall A B N, Π(A), B →→ N -> 

  exists C, exists D, N = Π(C), D /\ A →→ C /\ B →→ D.
1 subgoals, subgoal 1 (ID 8484)
  
  ============================
   forall A B N : Term,
   Π (A), B →→ N -> exists C D : Term, N = Π (C), D /\ (A →→ C) /\ B →→ D

(dependent evars:)





intros.
1 subgoals, subgoal 1 (ID 8488)
  
  A : Term
  B : Term
  N : Term
  H : Π (A), B →→ N
  ============================
   exists C D : Term, N = Π (C), D /\ (A →→ C) /\ B →→ D

(dependent evars:)





remember (Π(A), B) as P. 
1 subgoals, subgoal 1 (ID 8495)
  
  A : Term
  B : Term
  N : Term
  P : Term
  HeqP : P = Π (A), B
  H : P →→ N
  ============================
   exists C D : Term, N = Π (C), D /\ (A →→ C) /\ B →→ D

(dependent evars:)



revert A B HeqP; induction H; intros; subst; eauto.
2 subgoals, subgoal 1 (ID 8538)
  
  N : Term
  A : Term
  B : Term
  H : Π (A), B → N
  ============================
   exists C D : Term, N = Π (C), D /\ (A →→ C) /\ B →→ D

subgoal 2 (ID 8544) is:
 exists C D : Term, P = Π (C), D /\ (A →→ C) /\ B →→ D
(dependent evars: ?8545 using , ?8547 using ,)





inversion H; subst; clear H.
3 subgoals, subgoal 1 (ID 8754)
  
  A : Term
  B : Term
  B' : Term
  H3 : B → B'
  ============================
   exists C D : Term, Π (A), B' = Π (C), D /\ (A →→ C) /\ B →→ D

subgoal 2 (ID 8755) is:
 exists C D : Term, Π (A'), B = Π (C), D /\ (A →→ C) /\ B →→ D
subgoal 3 (ID 8544) is:
 exists C D : Term, P = Π (C), D /\ (A →→ C) /\ B →→ D
(dependent evars: ?8545 using , ?8547 using ,)





exists A; exists B'; intuition.
2 subgoals, subgoal 1 (ID 8755)
  
  A : Term
  B : Term
  A' : Term
  H3 : A → A'
  ============================
   exists C D : Term, Π (A'), B = Π (C), D /\ (A →→ C) /\ B →→ D

subgoal 2 (ID 8544) is:
 exists C D : Term, P = Π (C), D /\ (A →→ C) /\ B →→ D
(dependent evars: ?8545 using , ?8547 using ,)





exists A'; exists B; intuition.
1 subgoals, subgoal 1 (ID 8544)
  
  N : Term
  P : Term
  H0 : N →→ P
  IHBetas2 : forall A B : Term,
             N = Π (A), B ->
             exists C D : Term, P = Π (C), D /\ (A →→ C) /\ B →→ D
  A : Term
  B : Term
  H : Π (A), B →→ N
  IHBetas1 : forall A0 B0 : Term,
             Π (A), B = Π (A0), B0 ->
             exists C D : Term, N = Π (C), D /\ (A0 →→ C) /\ B0 →→ D
  ============================
   exists C D : Term, P = Π (C), D /\ (A →→ C) /\ B →→ D

(dependent evars: ?8545 using , ?8547 using ,)





destruct (IHBetas1 A B) as (C' & D' & ?); intuition.
1 subgoals, subgoal 1 (ID 8822)
  
  N : Term
  P : Term
  H0 : N →→ P
  IHBetas2 : forall A B : Term,
             N = Π (A), B ->
             exists C D : Term, P = Π (C), D /\ (A →→ C) /\ B →→ D
  A : Term
  B : Term
  H : Π (A), B →→ N
  IHBetas1 : forall A0 B0 : Term,
             Π (A), B = Π (A0), B0 ->
             exists C D : Term, N = Π (C), D /\ (A0 →→ C) /\ B0 →→ D
  C' : Term
  D' : Term
  H2 : N = Π (C'), D'
  H1 : A →→ C'
  H4 : B →→ D'
  ============================
   exists C D : Term, P = Π (C), D /\ (A →→ C) /\ B →→ D

(dependent evars: ?8545 using , ?8547 using ,)





destruct (IHBetas2 C' D') as (C'' & D'' &?); intuition.
1 subgoals, subgoal 1 (ID 8863)
  
  N : Term
  P : Term
  H0 : N →→ P
  IHBetas2 : forall A B : Term,
             N = Π (A), B ->
             exists C D : Term, P = Π (C), D /\ (A →→ C) /\ B →→ D
  A : Term
  B : Term
  H : Π (A), B →→ N
  IHBetas1 : forall A0 B0 : Term,
             Π (A), B = Π (A0), B0 ->
             exists C D : Term, N = Π (C), D /\ (A0 →→ C) /\ B0 →→ D
  C' : Term
  D' : Term
  H2 : N = Π (C'), D'
  H1 : A →→ C'
  H4 : B →→ D'
  C'' : Term
  D'' : Term
  H5 : P = Π (C''), D''
  H3 : C' →→ C''
  H7 : D' →→ D''
  ============================
   exists C D : Term, P = Π (C), D /\ (A →→ C) /\ B →→ D

(dependent evars: ?8545 using , ?8547 using ,)





exists C''; exists D''; eauto.
No more subgoals.
(dependent evars: ?8545 using , ?8547 using , ?8897 using , ?8909 using ,)





Qed.
Betas_Pi_inv is defined















Lift properties.





Lemma Beta_lift: forall M N  n m, M → N -> M ↑ n # m → N ↑ n # m .
1 subgoals, subgoal 1 (ID 8924)
  
  ============================
   forall (M N : Term) (n m : nat), M → N -> M ↑ n # m → N ↑ n # m

(dependent evars:)





intros.
1 subgoals, subgoal 1 (ID 8929)
  
  M : Term
  N : Term
  n : nat
  m : nat
  H : M → N
  ============================
   M ↑ n # m → N ↑ n # m

(dependent evars:)





generalize n m; clear n m.
1 subgoals, subgoal 1 (ID 8931)
  
  M : Term
  N : Term
  H : M → N
  ============================
   forall n m : nat, M ↑ n # m → N ↑ n # m

(dependent evars:)





induction H; intros; simpl; eauto.
1 subgoals, subgoal 1 (ID 9007)
  
  A : Term
  M : Term
  N : Term
  n : nat
  m : nat
  ============================
   (λ [A ↑ n # m], M ↑ n # (S m)) · N ↑ n # m → M [ ← N] ↑ n # m

(dependent evars:)





change m with (0+m).
1 subgoals, subgoal 1 (ID 9021)
  
  A : Term
  M : Term
  N : Term
  n : nat
  m : nat
  ============================
   (λ [A ↑ n # (0 + m)], M ↑ n # (S (0 + m))) · N ↑ n # (0 + m)
   → M [ ← N] ↑ n # (0 + m)

(dependent evars:)





rewrite substP1.
1 subgoals, subgoal 1 (ID 9022)
  
  A : Term
  M : Term
  N : Term
  n : nat
  m : nat
  ============================
   (λ [A ↑ n # (0 + m)], M ↑ n # (S (0 + m))) · N ↑ n # (0 + m)
   → (M ↑ n # (S (0 + m))) [ ← N ↑ n # m]

(dependent evars:)





constructor.
No more subgoals.
(dependent evars:)





Qed.
Beta_lift is defined








Lemma Betas_lift : forall M N n m , M →→ N -> M ↑ n # m →→ N ↑ n # m .
1 subgoals, subgoal 1 (ID 9028)
  
  ============================
   forall (M N : Term) (n m : nat), M →→ N -> M ↑ n # m →→ N ↑ n # m

(dependent evars:)





intros.
1 subgoals, subgoal 1 (ID 9033)
  
  M : Term
  N : Term
  n : nat
  m : nat
  H : M →→ N
  ============================
   M ↑ n # m →→ N ↑ n # m

(dependent evars:)





induction H.
3 subgoals, subgoal 1 (ID 9046)
  
  n : nat
  m : nat
  M : Term
  ============================
   M ↑ n # m →→ M ↑ n # m

subgoal 2 (ID 9049) is:
 M ↑ n # m →→ N ↑ n # m
subgoal 3 (ID 9057) is:
 M ↑ n # m →→ P ↑ n # m
(dependent evars:)





constructor.
2 subgoals, subgoal 1 (ID 9049)
  
  n : nat
  m : nat
  M : Term
  N : Term
  H : M → N
  ============================
   M ↑ n # m →→ N ↑ n # m

subgoal 2 (ID 9057) is:
 M ↑ n # m →→ P ↑ n # m
(dependent evars:)





constructor; apply Beta_lift; intuition.
1 subgoals, subgoal 1 (ID 9057)
  
  n : nat
  m : nat
  M : Term
  N : Term
  P : Term
  H : M →→ N
  H0 : N →→ P
  IHBetas1 : M ↑ n # m →→ N ↑ n # m
  IHBetas2 : N ↑ n # m →→ P ↑ n # m
  ============================
   M ↑ n # m →→ P ↑ n # m

(dependent evars:)





apply Betas_trans with (N:= N ↑ n # m ); intuition.
No more subgoals.
(dependent evars:)





Qed.
Betas_lift is defined








Lemma Betac_lift : forall M N n m, M ≡ N -> M ↑ n # m ≡ N ↑ n # m .
1 subgoals, subgoal 1 (ID 9069)
  
  ============================
   forall (M N : Term) (n m : nat), M ≡ N -> M ↑ n # m ≡ N ↑ n # m

(dependent evars:)





intros.
1 subgoals, subgoal 1 (ID 9074)
  
  M : Term
  N : Term
  n : nat
  m : nat
  H : M ≡ N
  ============================
   M ↑ n # m ≡ N ↑ n # m

(dependent evars:)





induction H.
3 subgoals, subgoal 1 (ID 9089)
  
  n : nat
  m : nat
  M : Term
  N : Term
  H : M →→ N
  ============================
   M ↑ n # m ≡ N ↑ n # m

subgoal 2 (ID 9093) is:
 N ↑ n # m ≡ M ↑ n # m
subgoal 3 (ID 9101) is:
 M ↑ n # m ≡ P ↑ n # m
(dependent evars:)





constructor.
3 subgoals, subgoal 1 (ID 9103)
  
  n : nat
  m : nat
  M : Term
  N : Term
  H : M →→ N
  ============================
   M ↑ n # m →→ N ↑ n # m

subgoal 2 (ID 9093) is:
 N ↑ n # m ≡ M ↑ n # m
subgoal 3 (ID 9101) is:
 M ↑ n # m ≡ P ↑ n # m
(dependent evars:)





apply Betas_lift; trivial.
2 subgoals, subgoal 1 (ID 9093)
  
  n : nat
  m : nat
  M : Term
  N : Term
  H : M ≡ N
  IHBetac : M ↑ n # m ≡ N ↑ n # m
  ============================
   N ↑ n # m ≡ M ↑ n # m

subgoal 2 (ID 9101) is:
 M ↑ n # m ≡ P ↑ n # m
(dependent evars:)





apply Betac_sym; trivial.
1 subgoals, subgoal 1 (ID 9101)
  
  n : nat
  m : nat
  M : Term
  N : Term
  P : Term
  H : M ≡ N
  H0 : N ≡ P
  IHBetac1 : M ↑ n # m ≡ N ↑ n # m
  IHBetac2 : N ↑ n # m ≡ P ↑ n # m
  ============================
   M ↑ n # m ≡ P ↑ n # m

(dependent evars:)





apply Betac_trans with (N ↑ n # m); trivial.
No more subgoals.
(dependent evars:)





Qed.
Betac_lift is defined








Hint Resolve Beta_lift Betas_lift Betac_lift.













Subst properties.





Lemma Betas_subst : forall M P P' n, P →→ P' -> M [n←P] →→ M[n← P'].
1 subgoals, subgoal 1 (ID 9112)
  
  ============================
   forall (M P P' : Term) (n : nat), P →→ P' -> M [n ← P] →→ M [n ← P']

(dependent evars:)





induction M; intros; simpl; eauto.
1 subgoals, subgoal 1 (ID 9161)
  
  v : Vars
  P : Term
  P' : Term
  n : nat
  H : P →→ P'
  ============================
   match lt_eq_lt_dec v n with
   | inleft (left _) => #v
   | inleft (right _) => P ↑ n
   | inright _ => #(v - 1)
   end
   →→ match lt_eq_lt_dec v n with
      | inleft (left _) => #v
      | inleft (right _) => P' ↑ n
      | inright _ => #(v - 1)
      end

(dependent evars:)





destruct (lt_eq_lt_dec v n); intuition.
No more subgoals.
(dependent evars:)





Qed.
Betas_subst is defined








Hint Resolve Betas_subst.






Lemma Betas_subst2 : forall M N P n, M →→ N -> M [n← P] →→ N [n ← P].
1 subgoals, subgoal 1 (ID 9540)
  
  ============================
   forall (M N P : Term) (n : nat), M →→ N -> M [n ← P] →→ N [n ← P]

(dependent evars:)





induction 1; eauto.
1 subgoals, subgoal 1 (ID 9561)
  
  P : Term
  n : nat
  M : Term
  N : Term
  H : M → N
  ============================
   M [n ← P] →→ N [n ← P]

(dependent evars: ?10360 using ,)





constructor. 
1 subgoals, subgoal 1 (ID 10377)
  
  P : Term
  n : nat
  M : Term
  N : Term
  H : M → N
  ============================
   M [n ← P] → N [n ← P]

(dependent evars: ?10360 using ,)



apply Beta_beta; intuition.
No more subgoals.
(dependent evars: ?10360 using ,)





Qed.
Betas_subst2 is defined








Hint Resolve Betas_subst2.






Lemma Betac_subst : forall M P P' n, P ≡ P' -> M[n←P] ≡ M [n←P'].
1 subgoals, subgoal 1 (ID 10383)
  
  ============================
   forall (M P P' : Term) (n : nat), P ≡ P' -> M [n ← P] ≡ M [n ← P']

(dependent evars:)





induction M; simpl; intros; intuition.
1 subgoals, subgoal 1 (ID 10420)
  
  v : Vars
  P : Term
  P' : Term
  n : nat
  H : P ≡ P'
  ============================
   match lt_eq_lt_dec v n with
   | inleft (left _) => #v
   | inleft (right _) => P ↑ n
   | inright _ => #(v - 1)
   end
   ≡ match lt_eq_lt_dec v n with
     | inleft (left _) => #v
     | inleft (right _) => P' ↑ n
     | inright _ => #(v - 1)
     end

(dependent evars:)





destruct (lt_eq_lt_dec v n); intuition.
No more subgoals.
(dependent evars:)





Qed.
Betac_subst is defined








Lemma Betac_subst2 : forall M N P n, 

  M ≡ N -> M[n←P] ≡ N[n← P] .
1 subgoals, subgoal 1 (ID 10627)
  
  ============================
   forall (M N P : Term) (n : nat), M ≡ N -> M [n ← P] ≡ N [n ← P]

(dependent evars:)





induction 1; eauto.
No more subgoals.
(dependent evars: ?10731 using ,)





Qed.
Betac_subst2 is defined








Hint Resolve Betac_subst Betac_subst2.














Parallel Reduction



We use the parallel reduction to prove that Beta is confluent.





Reserved Notation "M →' N" (at level 80).













Beta parallel definition. 





Inductive Betap : Term -> Term -> Prop :=

 | Betap_sort : forall s          , !s →' !s

 | Betap_var  : forall x          , #x →' #x

 | Betap_lam  : forall A A' M M'  , A →' A' -> M →' M' -> λ[A],M →' λ[A'],M'

 | Betap_pi   : forall A A' B B'  , A →' A' -> B →' B' -> Π(A),B →' Π(A'),B'

 | Betap_app  : forall M M' N N'  , M →' M' -> N →' N' -> M · N  →' M' · N'

 | Betap_head : forall A M M' N N', M →' M' -> N →' N' -> (λ[A],M)· N →' M'[← N']

where "M →' N" := (Betap M N) : UT_scope.
Betap is defined
Betap_ind is defined








Notation "m →' n" := (Betap m n) (at level 80) : UT_scope.
Warning: Notation _ →' _ was already used in scope UT_scope








Hint Constructors Betap.






Lemma Betap_refl : forall M, M →' M.
1 subgoals, subgoal 1 (ID 10815)
  
  ============================
   forall M : Term, M →' M

(dependent evars:)





induction M; eauto.
No more subgoals.
(dependent evars:)





Qed.
Betap_refl is defined








Hint Resolve Betap_refl.













Lift and Subst property of Betap.





Lemma Betap_lift: forall M N n m, M →' N -> M ↑ n # m →' N ↑ n # m .
1 subgoals, subgoal 1 (ID 10854)
  
  ============================
   forall (M N : Term) (n m : nat), M →' N -> M ↑ n # m →' N ↑ n # m

(dependent evars:)





intros.
1 subgoals, subgoal 1 (ID 10859)
  
  M : Term
  N : Term
  n : nat
  m : nat
  H : M →' N
  ============================
   M ↑ n # m →' N ↑ n # m

(dependent evars:)





revert n m.
1 subgoals, subgoal 1 (ID 10861)
  
  M : Term
  N : Term
  H : M →' N
  ============================
   forall n m : nat, M ↑ n # m →' N ↑ n # m

(dependent evars:)





induction H; simpl; intuition.
1 subgoals, subgoal 1 (ID 10989)
  
  A : Term
  M : Term
  M' : Term
  N : Term
  N' : Term
  H : M →' M'
  H0 : N →' N'
  IHBetap1 : forall n m : nat, M ↑ n # m →' M' ↑ n # m
  IHBetap2 : forall n m : nat, N ↑ n # m →' N' ↑ n # m
  n : nat
  m : nat
  ============================
   (λ [A ↑ n # m], M ↑ n # (S m)) · N ↑ n # m →' M' [ ← N'] ↑ n # m

(dependent evars:)





change m with (0+m).
1 subgoals, subgoal 1 (ID 11003)
  
  A : Term
  M : Term
  M' : Term
  N : Term
  N' : Term
  H : M →' M'
  H0 : N →' N'
  IHBetap1 : forall n m : nat, M ↑ n # m →' M' ↑ n # m
  IHBetap2 : forall n m : nat, N ↑ n # m →' N' ↑ n # m
  n : nat
  m : nat
  ============================
   (λ [A ↑ n # (0 + m)], M ↑ n # (S (0 + m))) · N ↑ n # (0 + m)
   →' M' [ ← N'] ↑ n # (0 + m)

(dependent evars:)





rewrite substP1.
1 subgoals, subgoal 1 (ID 11004)
  
  A : Term
  M : Term
  M' : Term
  N : Term
  N' : Term
  H : M →' M'
  H0 : N →' N'
  IHBetap1 : forall n m : nat, M ↑ n # m →' M' ↑ n # m
  IHBetap2 : forall n m : nat, N ↑ n # m →' N' ↑ n # m
  n : nat
  m : nat
  ============================
   (λ [A ↑ n # (0 + m)], M ↑ n # (S (0 + m))) · N ↑ n # (0 + m)
   →' (M' ↑ n # (S (0 + m))) [ ← N' ↑ n # m]

(dependent evars:)





constructor; intuition.
No more subgoals.
(dependent evars:)





Qed.
Betap_lift is defined








Hint Resolve Betap_lift.






Lemma Betap_subst:forall M M' N N' n, M →' M'  -> N →' N' -> M[n←N] →' M'[n←N'].
1 subgoals, subgoal 1 (ID 11042)
  
  ============================
   forall (M M' N N' : Term) (n : nat),
   M →' M' -> N →' N' -> M [n ← N] →' M' [n ← N']

(dependent evars:)





intros. 
1 subgoals, subgoal 1 (ID 11049)
  
  M : Term
  M' : Term
  N : Term
  N' : Term
  n : nat
  H : M →' M'
  H0 : N →' N'
  ============================
   M [n ← N] →' M' [n ← N']

(dependent evars:)



revert n.
1 subgoals, subgoal 1 (ID 11051)
  
  M : Term
  M' : Term
  N : Term
  N' : Term
  H : M →' M'
  H0 : N →' N'
  ============================
   forall n : nat, M [n ← N] →' M' [n ← N']

(dependent evars:)





induction H; simpl; intuition.
2 subgoals, subgoal 1 (ID 11151)
  
  N : Term
  N' : Term
  x : Vars
  H0 : N →' N'
  n : nat
  ============================
   match lt_eq_lt_dec x n with
   | inleft (left _) => #x
   | inleft (right _) => N ↑ n
   | inright _ => #(x - 1)
   end
   →' match lt_eq_lt_dec x n with
      | inleft (left _) => #x
      | inleft (right _) => N' ↑ n
      | inright _ => #(x - 1)
      end

subgoal 2 (ID 11206) is:
 (λ [A [n ← N]], M [(S n) ← N]) · N0 [n ← N] →' M' [ ← N'0] [n ← N']
(dependent evars:)





destruct lt_eq_lt_dec; intuition.
1 subgoals, subgoal 1 (ID 11206)
  
  N : Term
  N' : Term
  A : Term
  M : Term
  M' : Term
  N0 : Term
  N'0 : Term
  H : M →' M'
  H1 : N0 →' N'0
  H0 : N →' N'
  IHBetap1 : forall n : nat, M [n ← N] →' M' [n ← N']
  IHBetap2 : forall n : nat, N0 [n ← N] →' N'0 [n ← N']
  n : nat
  ============================
   (λ [A [n ← N]], M [(S n) ← N]) · N0 [n ← N] →' M' [ ← N'0] [n ← N']

(dependent evars:)





rewrite subst_travers. 
1 subgoals, subgoal 1 (ID 11259)
  
  N : Term
  N' : Term
  A : Term
  M : Term
  M' : Term
  N0 : Term
  N'0 : Term
  H : M →' M'
  H1 : N0 →' N'0
  H0 : N →' N'
  IHBetap1 : forall n : nat, M [n ← N] →' M' [n ← N']
  IHBetap2 : forall n : nat, N0 [n ← N] →' N'0 [n ← N']
  n : nat
  ============================
   (λ [A [n ← N]], M [(S n) ← N]) · N0 [n ← N]
   →' (M' [(n + 1) ← N']) [ ← N'0 [n ← N']]

(dependent evars:)



replace (S n) with (n+1) by (rewrite plus_comm; trivial). 
1 subgoals, subgoal 1 (ID 11263)
  
  N : Term
  N' : Term
  A : Term
  M : Term
  M' : Term
  N0 : Term
  N'0 : Term
  H : M →' M'
  H1 : N0 →' N'0
  H0 : N →' N'
  IHBetap1 : forall n : nat, M [n ← N] →' M' [n ← N']
  IHBetap2 : forall n : nat, N0 [n ← N] →' N'0 [n ← N']
  n : nat
  ============================
   (λ [A [n ← N]], M [(n + 1) ← N]) · N0 [n ← N]
   →' (M' [(n + 1) ← N']) [ ← N'0 [n ← N']]

(dependent evars:)



constructor; intuition.
No more subgoals.
(dependent evars:)





Qed.
Betap_subst is defined








Hint Resolve Betap_subst.













Betap has the diamond property. 





Lemma Betap_diamond : forall M N P,

   M →' N -> M →' P -> exists Q, N →' Q /\ P →' Q.
1 subgoals, subgoal 1 (ID 11306)
  
  ============================
   forall M N P : Term,
   M →' N -> M →' P -> exists Q : Term, (N →' Q) /\ P →' Q

(dependent evars:)





intros.
1 subgoals, subgoal 1 (ID 11311)
  
  M : Term
  N : Term
  P : Term
  H : M →' N
  H0 : M →' P
  ============================
   exists Q : Term, (N →' Q) /\ P →' Q

(dependent evars:)





revert P H0.
1 subgoals, subgoal 1 (ID 11313)
  
  M : Term
  N : Term
  H : M →' N
  ============================
   forall P : Term, M →' P -> exists Q : Term, (N →' Q) /\ P →' Q

(dependent evars:)





induction H; intros.
6 subgoals, subgoal 1 (ID 11378)
  
  s : X.Sorts
  P : Term
  H0 : !s →' P
  ============================
   exists Q : Term, (!s →' Q) /\ P →' Q

subgoal 2 (ID 11380) is:
 exists Q : Term, (#x →' Q) /\ P →' Q
subgoal 3 (ID 11382) is:
 exists Q : Term, (λ [A'], M' →' Q) /\ P →' Q
subgoal 4 (ID 11384) is:
 exists Q : Term, (Π (A'), B' →' Q) /\ P →' Q
subgoal 5 (ID 11386) is:
 exists Q : Term, (M' · N' →' Q) /\ P →' Q
subgoal 6 (ID 11388) is:
 exists Q : Term, (M' [ ← N'] →' Q) /\ P →' Q
(dependent evars:)





exists P; intuition.
5 subgoals, subgoal 1 (ID 11380)
  
  x : Vars
  P : Term
  H0 : #x →' P
  ============================
   exists Q : Term, (#x →' Q) /\ P →' Q

subgoal 2 (ID 11382) is:
 exists Q : Term, (λ [A'], M' →' Q) /\ P →' Q
subgoal 3 (ID 11384) is:
 exists Q : Term, (Π (A'), B' →' Q) /\ P →' Q
subgoal 4 (ID 11386) is:
 exists Q : Term, (M' · N' →' Q) /\ P →' Q
subgoal 5 (ID 11388) is:
 exists Q : Term, (M' [ ← N'] →' Q) /\ P →' Q
(dependent evars:)





exists P; intuition.
4 subgoals, subgoal 1 (ID 11382)
  
  A : Term
  A' : Term
  M : Term
  M' : Term
  H : A →' A'
  H0 : M →' M'
  IHBetap1 : forall P : Term, A →' P -> exists Q : Term, (A' →' Q) /\ P →' Q
  IHBetap2 : forall P : Term, M →' P -> exists Q : Term, (M' →' Q) /\ P →' Q
  P : Term
  H1 : λ [A], M →' P
  ============================
   exists Q : Term, (λ [A'], M' →' Q) /\ P →' Q

subgoal 2 (ID 11384) is:
 exists Q : Term, (Π (A'), B' →' Q) /\ P →' Q
subgoal 3 (ID 11386) is:
 exists Q : Term, (M' · N' →' Q) /\ P →' Q
subgoal 4 (ID 11388) is:
 exists Q : Term, (M' [ ← N'] →' Q) /\ P →' Q
(dependent evars:)





inversion H1; subst; clear H1.
4 subgoals, subgoal 1 (ID 11543)
  
  A : Term
  A' : Term
  M : Term
  M' : Term
  H : A →' A'
  H0 : M →' M'
  IHBetap1 : forall P : Term, A →' P -> exists Q : Term, (A' →' Q) /\ P →' Q
  IHBetap2 : forall P : Term, M →' P -> exists Q : Term, (M' →' Q) /\ P →' Q
  A'0 : Term
  M'0 : Term
  H4 : A →' A'0
  H6 : M →' M'0
  ============================
   exists Q : Term, (λ [A'], M' →' Q) /\ λ [A'0], M'0 →' Q

subgoal 2 (ID 11384) is:
 exists Q : Term, (Π (A'), B' →' Q) /\ P →' Q
subgoal 3 (ID 11386) is:
 exists Q : Term, (M' · N' →' Q) /\ P →' Q
subgoal 4 (ID 11388) is:
 exists Q : Term, (M' [ ← N'] →' Q) /\ P →' Q
(dependent evars:)





destruct (IHBetap1 A'0 H4) as (A'' & ? & ?).
4 subgoals, subgoal 1 (ID 11554)
  
  A : Term
  A' : Term
  M : Term
  M' : Term
  H : A →' A'
  H0 : M →' M'
  IHBetap1 : forall P : Term, A →' P -> exists Q : Term, (A' →' Q) /\ P →' Q
  IHBetap2 : forall P : Term, M →' P -> exists Q : Term, (M' →' Q) /\ P →' Q
  A'0 : Term
  M'0 : Term
  H4 : A →' A'0
  H6 : M →' M'0
  A'' : Term
  H1 : A' →' A''
  H2 : A'0 →' A''
  ============================
   exists Q : Term, (λ [A'], M' →' Q) /\ λ [A'0], M'0 →' Q

subgoal 2 (ID 11384) is:
 exists Q : Term, (Π (A'), B' →' Q) /\ P →' Q
subgoal 3 (ID 11386) is:
 exists Q : Term, (M' · N' →' Q) /\ P →' Q
subgoal 4 (ID 11388) is:
 exists Q : Term, (M' [ ← N'] →' Q) /\ P →' Q
(dependent evars:)





destruct (IHBetap2 M'0 H6) as (M'' & ?& ?).
4 subgoals, subgoal 1 (ID 11565)
  
  A : Term
  A' : Term
  M : Term
  M' : Term
  H : A →' A'
  H0 : M →' M'
  IHBetap1 : forall P : Term, A →' P -> exists Q : Term, (A' →' Q) /\ P →' Q
  IHBetap2 : forall P : Term, M →' P -> exists Q : Term, (M' →' Q) /\ P →' Q
  A'0 : Term
  M'0 : Term
  H4 : A →' A'0
  H6 : M →' M'0
  A'' : Term
  H1 : A' →' A''
  H2 : A'0 →' A''
  M'' : Term
  H3 : M' →' M''
  H5 : M'0 →' M''
  ============================
   exists Q : Term, (λ [A'], M' →' Q) /\ λ [A'0], M'0 →' Q

subgoal 2 (ID 11384) is:
 exists Q : Term, (Π (A'), B' →' Q) /\ P →' Q
subgoal 3 (ID 11386) is:
 exists Q : Term, (M' · N' →' Q) /\ P →' Q
subgoal 4 (ID 11388) is:
 exists Q : Term, (M' [ ← N'] →' Q) /\ P →' Q
(dependent evars:)





exists (λ[A''],M''); intuition.
3 subgoals, subgoal 1 (ID 11384)
  
  A : Term
  A' : Term
  B : Term
  B' : Term
  H : A →' A'
  H0 : B →' B'
  IHBetap1 : forall P : Term, A →' P -> exists Q : Term, (A' →' Q) /\ P →' Q
  IHBetap2 : forall P : Term, B →' P -> exists Q : Term, (B' →' Q) /\ P →' Q
  P : Term
  H1 : Π (A), B →' P
  ============================
   exists Q : Term, (Π (A'), B' →' Q) /\ P →' Q

subgoal 2 (ID 11386) is:
 exists Q : Term, (M' · N' →' Q) /\ P →' Q
subgoal 3 (ID 11388) is:
 exists Q : Term, (M' [ ← N'] →' Q) /\ P →' Q
(dependent evars:)





inversion H1; subst; clear H1.
3 subgoals, subgoal 1 (ID 11749)
  
  A : Term
  A' : Term
  B : Term
  B' : Term
  H : A →' A'
  H0 : B →' B'
  IHBetap1 : forall P : Term, A →' P -> exists Q : Term, (A' →' Q) /\ P →' Q
  IHBetap2 : forall P : Term, B →' P -> exists Q : Term, (B' →' Q) /\ P →' Q
  A'0 : Term
  B'0 : Term
  H4 : A →' A'0
  H6 : B →' B'0
  ============================
   exists Q : Term, (Π (A'), B' →' Q) /\ Π (A'0), B'0 →' Q

subgoal 2 (ID 11386) is:
 exists Q : Term, (M' · N' →' Q) /\ P →' Q
subgoal 3 (ID 11388) is:
 exists Q : Term, (M' [ ← N'] →' Q) /\ P →' Q
(dependent evars:)





destruct (IHBetap1 A'0 H4) as (A'' & ? & ?).
3 subgoals, subgoal 1 (ID 11760)
  
  A : Term
  A' : Term
  B : Term
  B' : Term
  H : A →' A'
  H0 : B →' B'
  IHBetap1 : forall P : Term, A →' P -> exists Q : Term, (A' →' Q) /\ P →' Q
  IHBetap2 : forall P : Term, B →' P -> exists Q : Term, (B' →' Q) /\ P →' Q
  A'0 : Term
  B'0 : Term
  H4 : A →' A'0
  H6 : B →' B'0
  A'' : Term
  H1 : A' →' A''
  H2 : A'0 →' A''
  ============================
   exists Q : Term, (Π (A'), B' →' Q) /\ Π (A'0), B'0 →' Q

subgoal 2 (ID 11386) is:
 exists Q : Term, (M' · N' →' Q) /\ P →' Q
subgoal 3 (ID 11388) is:
 exists Q : Term, (M' [ ← N'] →' Q) /\ P →' Q
(dependent evars:)





destruct (IHBetap2 B'0 H6) as (B'' & ?& ?).
3 subgoals, subgoal 1 (ID 11771)
  
  A : Term
  A' : Term
  B : Term
  B' : Term
  H : A →' A'
  H0 : B →' B'
  IHBetap1 : forall P : Term, A →' P -> exists Q : Term, (A' →' Q) /\ P →' Q
  IHBetap2 : forall P : Term, B →' P -> exists Q : Term, (B' →' Q) /\ P →' Q
  A'0 : Term
  B'0 : Term
  H4 : A →' A'0
  H6 : B →' B'0
  A'' : Term
  H1 : A' →' A''
  H2 : A'0 →' A''
  B'' : Term
  H3 : B' →' B''
  H5 : B'0 →' B''
  ============================
   exists Q : Term, (Π (A'), B' →' Q) /\ Π (A'0), B'0 →' Q

subgoal 2 (ID 11386) is:
 exists Q : Term, (M' · N' →' Q) /\ P →' Q
subgoal 3 (ID 11388) is:
 exists Q : Term, (M' [ ← N'] →' Q) /\ P →' Q
(dependent evars:)





exists (Π(A''), B''); intuition.
2 subgoals, subgoal 1 (ID 11386)
  
  M : Term
  M' : Term
  N : Term
  N' : Term
  H : M →' M'
  H0 : N →' N'
  IHBetap1 : forall P : Term, M →' P -> exists Q : Term, (M' →' Q) /\ P →' Q
  IHBetap2 : forall P : Term, N →' P -> exists Q : Term, (N' →' Q) /\ P →' Q
  P : Term
  H1 : M · N →' P
  ============================
   exists Q : Term, (M' · N' →' Q) /\ P →' Q

subgoal 2 (ID 11388) is:
 exists Q : Term, (M' [ ← N'] →' Q) /\ P →' Q
(dependent evars:)





inversion H1; subst; clear H1.
3 subgoals, subgoal 1 (ID 11986)
  
  M : Term
  M' : Term
  N : Term
  N' : Term
  H : M →' M'
  H0 : N →' N'
  IHBetap1 : forall P : Term, M →' P -> exists Q : Term, (M' →' Q) /\ P →' Q
  IHBetap2 : forall P : Term, N →' P -> exists Q : Term, (N' →' Q) /\ P →' Q
  M'0 : Term
  N'0 : Term
  H4 : M →' M'0
  H6 : N →' N'0
  ============================
   exists Q : Term, (M' · N' →' Q) /\ M'0 · N'0 →' Q

subgoal 2 (ID 11987) is:
 exists Q : Term, (M' · N' →' Q) /\ M'0 [ ← N'0] →' Q
subgoal 3 (ID 11388) is:
 exists Q : Term, (M' [ ← N'] →' Q) /\ P →' Q
(dependent evars:)





destruct (IHBetap1 M'0 H4) as (M'' & ?& ?).
3 subgoals, subgoal 1 (ID 11998)
  
  M : Term
  M' : Term
  N : Term
  N' : Term
  H : M →' M'
  H0 : N →' N'
  IHBetap1 : forall P : Term, M →' P -> exists Q : Term, (M' →' Q) /\ P →' Q
  IHBetap2 : forall P : Term, N →' P -> exists Q : Term, (N' →' Q) /\ P →' Q
  M'0 : Term
  N'0 : Term
  H4 : M →' M'0
  H6 : N →' N'0
  M'' : Term
  H1 : M' →' M''
  H2 : M'0 →' M''
  ============================
   exists Q : Term, (M' · N' →' Q) /\ M'0 · N'0 →' Q

subgoal 2 (ID 11987) is:
 exists Q : Term, (M' · N' →' Q) /\ M'0 [ ← N'0] →' Q
subgoal 3 (ID 11388) is:
 exists Q : Term, (M' [ ← N'] →' Q) /\ P →' Q
(dependent evars:)





destruct (IHBetap2 N'0 H6) as (N'' & ?& ?).
3 subgoals, subgoal 1 (ID 12009)
  
  M : Term
  M' : Term
  N : Term
  N' : Term
  H : M →' M'
  H0 : N →' N'
  IHBetap1 : forall P : Term, M →' P -> exists Q : Term, (M' →' Q) /\ P →' Q
  IHBetap2 : forall P : Term, N →' P -> exists Q : Term, (N' →' Q) /\ P →' Q
  M'0 : Term
  N'0 : Term
  H4 : M →' M'0
  H6 : N →' N'0
  M'' : Term
  H1 : M' →' M''
  H2 : M'0 →' M''
  N'' : Term
  H3 : N' →' N''
  H5 : N'0 →' N''
  ============================
   exists Q : Term, (M' · N' →' Q) /\ M'0 · N'0 →' Q

subgoal 2 (ID 11987) is:
 exists Q : Term, (M' · N' →' Q) /\ M'0 [ ← N'0] →' Q
subgoal 3 (ID 11388) is:
 exists Q : Term, (M' [ ← N'] →' Q) /\ P →' Q
(dependent evars:)





exists (M'' · N''); intuition.
2 subgoals, subgoal 1 (ID 11987)
  
  M' : Term
  N : Term
  N' : Term
  H0 : N →' N'
  IHBetap2 : forall P : Term, N →' P -> exists Q : Term, (N' →' Q) /\ P →' Q
  A : Term
  M0 : Term
  M'0 : Term
  N'0 : Term
  H4 : M0 →' M'0
  H6 : N →' N'0
  H : λ [A], M0 →' M'
  IHBetap1 : forall P : Term,
             λ [A], M0 →' P -> exists Q : Term, (M' →' Q) /\ P →' Q
  ============================
   exists Q : Term, (M' · N' →' Q) /\ M'0 [ ← N'0] →' Q

subgoal 2 (ID 11388) is:
 exists Q : Term, (M' [ ← N'] →' Q) /\ P →' Q
(dependent evars:)





inversion H; subst; clear H.
2 subgoals, subgoal 1 (ID 12194)
  
  N : Term
  N' : Term
  H0 : N →' N'
  IHBetap2 : forall P : Term, N →' P -> exists Q : Term, (N' →' Q) /\ P →' Q
  A : Term
  M0 : Term
  M'0 : Term
  N'0 : Term
  H4 : M0 →' M'0
  H6 : N →' N'0
  A' : Term
  M'1 : Term
  H3 : A →' A'
  H7 : M0 →' M'1
  IHBetap1 : forall P : Term,
             λ [A], M0 →' P -> exists Q : Term, (λ [A'], M'1 →' Q) /\ P →' Q
  ============================
   exists Q : Term, ((λ [A'], M'1) · N' →' Q) /\ M'0 [ ← N'0] →' Q

subgoal 2 (ID 11388) is:
 exists Q : Term, (M' [ ← N'] →' Q) /\ P →' Q
(dependent evars:)





destruct (IHBetap2 N'0 H6) as (N'' & ?& ?).
2 subgoals, subgoal 1 (ID 12205)
  
  N : Term
  N' : Term
  H0 : N →' N'
  IHBetap2 : forall P : Term, N →' P -> exists Q : Term, (N' →' Q) /\ P →' Q
  A : Term
  M0 : Term
  M'0 : Term
  N'0 : Term
  H4 : M0 →' M'0
  H6 : N →' N'0
  A' : Term
  M'1 : Term
  H3 : A →' A'
  H7 : M0 →' M'1
  IHBetap1 : forall P : Term,
             λ [A], M0 →' P -> exists Q : Term, (λ [A'], M'1 →' Q) /\ P →' Q
  N'' : Term
  H : N' →' N''
  H1 : N'0 →' N''
  ============================
   exists Q : Term, ((λ [A'], M'1) · N' →' Q) /\ M'0 [ ← N'0] →' Q

subgoal 2 (ID 11388) is:
 exists Q : Term, (M' [ ← N'] →' Q) /\ P →' Q
(dependent evars:)





destruct (IHBetap1 (λ[A],M'0)) as  (L & ?& ?); intuition.
2 subgoals, subgoal 1 (ID 12219)
  
  N : Term
  N' : Term
  H0 : N →' N'
  IHBetap2 : forall P : Term, N →' P -> exists Q : Term, (N' →' Q) /\ P →' Q
  A : Term
  M0 : Term
  M'0 : Term
  N'0 : Term
  H4 : M0 →' M'0
  H6 : N →' N'0
  A' : Term
  M'1 : Term
  H3 : A →' A'
  H7 : M0 →' M'1
  IHBetap1 : forall P : Term,
             λ [A], M0 →' P -> exists Q : Term, (λ [A'], M'1 →' Q) /\ P →' Q
  N'' : Term
  H : N' →' N''
  H1 : N'0 →' N''
  L : Term
  H2 : λ [A'], M'1 →' L
  H5 : λ [A], M'0 →' L
  ============================
   exists Q : Term, ((λ [A'], M'1) · N' →' Q) /\ M'0 [ ← N'0] →' Q

subgoal 2 (ID 11388) is:
 exists Q : Term, (M' [ ← N'] →' Q) /\ P →' Q
(dependent evars:)





inversion H2; subst; clear H2; inversion H5; subst; clear H5.
2 subgoals, subgoal 1 (ID 12547)
  
  N : Term
  N' : Term
  H0 : N →' N'
  IHBetap2 : forall P : Term, N →' P -> exists Q : Term, (N' →' Q) /\ P →' Q
  A : Term
  M0 : Term
  M'0 : Term
  N'0 : Term
  H4 : M0 →' M'0
  H6 : N →' N'0
  A' : Term
  M'1 : Term
  H3 : A →' A'
  H7 : M0 →' M'1
  IHBetap1 : forall P : Term,
             λ [A], M0 →' P -> exists Q : Term, (λ [A'], M'1 →' Q) /\ P →' Q
  N'' : Term
  H : N' →' N''
  H1 : N'0 →' N''
  A'0 : Term
  M' : Term
  H10 : A' →' A'0
  H12 : M'1 →' M'
  H11 : A →' A'0
  H14 : M'0 →' M'
  ============================
   exists Q : Term, ((λ [A'], M'1) · N' →' Q) /\ M'0 [ ← N'0] →' Q

subgoal 2 (ID 11388) is:
 exists Q : Term, (M' [ ← N'] →' Q) /\ P →' Q
(dependent evars:)





exists ( M' [ ← N'']); intuition.
1 subgoals, subgoal 1 (ID 11388)
  
  A : Term
  M : Term
  M' : Term
  N : Term
  N' : Term
  H : M →' M'
  H0 : N →' N'
  IHBetap1 : forall P : Term, M →' P -> exists Q : Term, (M' →' Q) /\ P →' Q
  IHBetap2 : forall P : Term, N →' P -> exists Q : Term, (N' →' Q) /\ P →' Q
  P : Term
  H1 : (λ [A], M) · N →' P
  ============================
   exists Q : Term, (M' [ ← N'] →' Q) /\ P →' Q

(dependent evars:)





inversion H1; subst; clear H1.
2 subgoals, subgoal 1 (ID 12778)
  
  A : Term
  M : Term
  M' : Term
  N : Term
  N' : Term
  H : M →' M'
  H0 : N →' N'
  IHBetap1 : forall P : Term, M →' P -> exists Q : Term, (M' →' Q) /\ P →' Q
  IHBetap2 : forall P : Term, N →' P -> exists Q : Term, (N' →' Q) /\ P →' Q
  M'0 : Term
  N'0 : Term
  H4 : λ [A], M →' M'0
  H6 : N →' N'0
  ============================
   exists Q : Term, (M' [ ← N'] →' Q) /\ M'0 · N'0 →' Q

subgoal 2 (ID 12779) is:
 exists Q : Term, (M' [ ← N'] →' Q) /\ M'0 [ ← N'0] →' Q
(dependent evars:)





destruct (IHBetap2 N'0 H6) as (N'' & ?& ?).
2 subgoals, subgoal 1 (ID 12790)
  
  A : Term
  M : Term
  M' : Term
  N : Term
  N' : Term
  H : M →' M'
  H0 : N →' N'
  IHBetap1 : forall P : Term, M →' P -> exists Q : Term, (M' →' Q) /\ P →' Q
  IHBetap2 : forall P : Term, N →' P -> exists Q : Term, (N' →' Q) /\ P →' Q
  M'0 : Term
  N'0 : Term
  H4 : λ [A], M →' M'0
  H6 : N →' N'0
  N'' : Term
  H1 : N' →' N''
  H2 : N'0 →' N''
  ============================
   exists Q : Term, (M' [ ← N'] →' Q) /\ M'0 · N'0 →' Q

subgoal 2 (ID 12779) is:
 exists Q : Term, (M' [ ← N'] →' Q) /\ M'0 [ ← N'0] →' Q
(dependent evars:)





inversion H4; subst; clear H4.
2 subgoals, subgoal 1 (ID 12927)
  
  A : Term
  M : Term
  M' : Term
  N : Term
  N' : Term
  H : M →' M'
  H0 : N →' N'
  IHBetap1 : forall P : Term, M →' P -> exists Q : Term, (M' →' Q) /\ P →' Q
  IHBetap2 : forall P : Term, N →' P -> exists Q : Term, (N' →' Q) /\ P →' Q
  N'0 : Term
  H6 : N →' N'0
  N'' : Term
  H1 : N' →' N''
  H2 : N'0 →' N''
  A' : Term
  M'1 : Term
  H7 : A →' A'
  H9 : M →' M'1
  ============================
   exists Q : Term, (M' [ ← N'] →' Q) /\ (λ [A'], M'1) · N'0 →' Q

subgoal 2 (ID 12779) is:
 exists Q : Term, (M' [ ← N'] →' Q) /\ M'0 [ ← N'0] →' Q
(dependent evars:)





destruct (IHBetap1 M'1 H9) as (M'' & ?& ?).
2 subgoals, subgoal 1 (ID 12938)
  
  A : Term
  M : Term
  M' : Term
  N : Term
  N' : Term
  H : M →' M'
  H0 : N →' N'
  IHBetap1 : forall P : Term, M →' P -> exists Q : Term, (M' →' Q) /\ P →' Q
  IHBetap2 : forall P : Term, N →' P -> exists Q : Term, (N' →' Q) /\ P →' Q
  N'0 : Term
  H6 : N →' N'0
  N'' : Term
  H1 : N' →' N''
  H2 : N'0 →' N''
  A' : Term
  M'1 : Term
  H7 : A →' A'
  H9 : M →' M'1
  M'' : Term
  H3 : M' →' M''
  H4 : M'1 →' M''
  ============================
   exists Q : Term, (M' [ ← N'] →' Q) /\ (λ [A'], M'1) · N'0 →' Q

subgoal 2 (ID 12779) is:
 exists Q : Term, (M' [ ← N'] →' Q) /\ M'0 [ ← N'0] →' Q
(dependent evars:)





exists (M''[← N'']); intuition.
1 subgoals, subgoal 1 (ID 12779)
  
  A : Term
  M : Term
  M' : Term
  N : Term
  N' : Term
  H : M →' M'
  H0 : N →' N'
  IHBetap1 : forall P : Term, M →' P -> exists Q : Term, (M' →' Q) /\ P →' Q
  IHBetap2 : forall P : Term, N →' P -> exists Q : Term, (N' →' Q) /\ P →' Q
  M'0 : Term
  N'0 : Term
  H6 : M →' M'0
  H7 : N →' N'0
  ============================
   exists Q : Term, (M' [ ← N'] →' Q) /\ M'0 [ ← N'0] →' Q

(dependent evars:)





destruct (IHBetap2 N'0 H7) as (N'' & ?& ?).
1 subgoals, subgoal 1 (ID 13002)
  
  A : Term
  M : Term
  M' : Term
  N : Term
  N' : Term
  H : M →' M'
  H0 : N →' N'
  IHBetap1 : forall P : Term, M →' P -> exists Q : Term, (M' →' Q) /\ P →' Q
  IHBetap2 : forall P : Term, N →' P -> exists Q : Term, (N' →' Q) /\ P →' Q
  M'0 : Term
  N'0 : Term
  H6 : M →' M'0
  H7 : N →' N'0
  N'' : Term
  H1 : N' →' N''
  H2 : N'0 →' N''
  ============================
   exists Q : Term, (M' [ ← N'] →' Q) /\ M'0 [ ← N'0] →' Q

(dependent evars:)





destruct (IHBetap1 M'0 H6) as (M'' & ?& ?).
1 subgoals, subgoal 1 (ID 13013)
  
  A : Term
  M : Term
  M' : Term
  N : Term
  N' : Term
  H : M →' M'
  H0 : N →' N'
  IHBetap1 : forall P : Term, M →' P -> exists Q : Term, (M' →' Q) /\ P →' Q
  IHBetap2 : forall P : Term, N →' P -> exists Q : Term, (N' →' Q) /\ P →' Q
  M'0 : Term
  N'0 : Term
  H6 : M →' M'0
  H7 : N →' N'0
  N'' : Term
  H1 : N' →' N''
  H2 : N'0 →' N''
  M'' : Term
  H3 : M' →' M''
  H4 : M'0 →' M''
  ============================
   exists Q : Term, (M' [ ← N'] →' Q) /\ M'0 [ ← N'0] →' Q

(dependent evars:)





exists (M''[← N'']); intuition.
No more subgoals.
(dependent evars:)





Qed.
Betap_diamond is defined















Reflexive Transitive closure of Betap.





Reserved Notation " x  →→' y " (at level 80).






Inductive Betaps : Term -> Term -> Prop :=

 | Betaps_refl  : forall M    , M →→' M

 | Betaps_trans : forall M N P, M  →' N -> N  →→' P -> M  →→' P

where " x  →→' y " := (Betaps x y) : UT_scope.
Betaps is defined
Betaps_ind is defined








Hint Constructors Betaps.
Warning: the hint: eapply Betaps_trans will only be used by eauto















Closure properties to relate Betaps and Betas.





Lemma Betas_Betap_closure : forall M N , M →' N -> M →→ N.
1 subgoals, subgoal 1 (ID 13069)
  
  ============================
   forall M N : Term, M →' N -> M →→ N

(dependent evars:)





induction 1; eauto.
No more subgoals.
(dependent evars: ?13187 using ?13192 ?13191 , ?13191 using ?13726 ?13725 , ?13192 using , ?13725 using , ?13726 using ,)





Qed.
Betas_Betap_closure is defined








Local Hint Resolve Betas_Betap_closure.






Lemma Betas_Betaps_closure : forall M N,  M →→' N -> M →→  N.
1 subgoals, subgoal 1 (ID 14049)
  
  ============================
   forall M N : Term, M →→' N -> M →→ N

(dependent evars:)





induction 1; eauto.
No more subgoals.
(dependent evars: ?14075 using , ?14085 using , ?14095 using ,)





Qed.
Betas_Betaps_closure is defined








Lemma Betap_Beta_closure : forall M N, M → N -> M →' N.
1 subgoals, subgoal 1 (ID 14125)
  
  ============================
   forall M N : Term, M → N -> M →' N

(dependent evars:)





induction 1; intuition.
No more subgoals.
(dependent evars:)





Qed.
Betap_Beta_closure is defined








Local Hint Resolve Betas_Betaps_closure Betap_Beta_closure.






Lemma Betaps_Beta_closure :forall M N, M → N -> M →→' N.
1 subgoals, subgoal 1 (ID 14246)
  
  ============================
   forall M N : Term, M → N -> M →→' N

(dependent evars:)





eauto.
No more subgoals.
(dependent evars: ?14250 using , ?14254 using , ?14258 using ,)





Qed.
Betaps_Beta_closure is defined








Local Hint Resolve Betaps_Beta_closure.






Lemma Betaps_trans2 : forall M N P, M →→' N -> N →→' P  -> M →→' P.
1 subgoals, subgoal 1 (ID 14275)
  
  ============================
   forall M N P : Term, M →→' N -> N →→' P -> M →→' P

(dependent evars:)





intros. 
1 subgoals, subgoal 1 (ID 14280)
  
  M : Term
  N : Term
  P : Term
  H : M →→' N
  H0 : N →→' P
  ============================
   M →→' P

(dependent evars:)



revert P H0; induction H; eauto.
No more subgoals.
(dependent evars: ?14307 using ,)





Qed.
Betaps_trans2 is defined








Local Hint Resolve Betaps_trans2.
Warning: the hint: eapply Betaps_trans2 will only be used by eauto








Lemma Betaps_Betas_closure : forall M N , M →→ N -> M →→' N.
1 subgoals, subgoal 1 (ID 14322)
  
  ============================
   forall M N : Term, M →→ N -> M →→' N

(dependent evars:)





induction 1; eauto.
No more subgoals.
(dependent evars: ?14365 using ,)





Qed.
Betaps_Betas_closure is defined








Local Hint Resolve Betaps_Betas_closure.













Betas inherites its diamond property from Betaps.





Lemma sub_diamond_Betaps : 

(   forall M N P, M →' N -> M →'  P -> exists Q, N →'  Q /\ P →' Q )

 -> forall M N P, M →' N -> M →→' P -> exists Q, N →→' Q /\ P →' Q .
1 subgoals, subgoal 1 (ID 14393)
  
  ============================
   (forall M N P : Term,
    M →' N -> M →' P -> exists Q : Term, (N →' Q) /\ P →' Q) ->
   forall M N P : Term,
   M →' N -> M →→' P -> exists Q : Term, (N →→' Q) /\ P →' Q

(dependent evars:)





intros.
1 subgoals, subgoal 1 (ID 14399)
  
  H : forall M N P : Term,
      M →' N -> M →' P -> exists Q : Term, (N →' Q) /\ P →' Q
  M : Term
  N : Term
  P : Term
  H0 : M →' N
  H1 : M →→' P
  ============================
   exists Q : Term, (N →→' Q) /\ P →' Q

(dependent evars:)





revert N H0. 
1 subgoals, subgoal 1 (ID 14401)
  
  H : forall M N P : Term,
      M →' N -> M →' P -> exists Q : Term, (N →' Q) /\ P →' Q
  M : Term
  P : Term
  H1 : M →→' P
  ============================
   forall N : Term, M →' N -> exists Q : Term, (N →→' Q) /\ P →' Q

(dependent evars:)



induction H1; eauto.
1 subgoals, subgoal 1 (ID 14416)
  
  H : forall M N P : Term,
      M →' N -> M →' P -> exists Q : Term, (N →' Q) /\ P →' Q
  M : Term
  N : Term
  P : Term
  H0 : M →' N
  H1 : N →→' P
  IHBetaps : forall N0 : Term,
             N →' N0 -> exists Q : Term, (N0 →→' Q) /\ P →' Q
  ============================
   forall N0 : Term, M →' N0 -> exists Q : Term, (N0 →→' Q) /\ P →' Q

(dependent evars: ?14419 using ,)





intros.
1 subgoals, subgoal 1 (ID 14634)
  
  H : forall M N P : Term,
      M →' N -> M →' P -> exists Q : Term, (N →' Q) /\ P →' Q
  M : Term
  N : Term
  P : Term
  H0 : M →' N
  H1 : N →→' P
  IHBetaps : forall N0 : Term,
             N →' N0 -> exists Q : Term, (N0 →→' Q) /\ P →' Q
  N0 : Term
  H2 : M →' N0
  ============================
   exists Q : Term, (N0 →→' Q) /\ P →' Q

(dependent evars: ?14419 using ,)





destruct (H M N N0 H0 H2) as (Q & ?& ?).
1 subgoals, subgoal 1 (ID 14645)
  
  H : forall M N P : Term,
      M →' N -> M →' P -> exists Q : Term, (N →' Q) /\ P →' Q
  M : Term
  N : Term
  P : Term
  H0 : M →' N
  H1 : N →→' P
  IHBetaps : forall N0 : Term,
             N →' N0 -> exists Q : Term, (N0 →→' Q) /\ P →' Q
  N0 : Term
  H2 : M →' N0
  Q : Term
  H3 : N →' Q
  H4 : N0 →' Q
  ============================
   exists Q0 : Term, (N0 →→' Q0) /\ P →' Q0

(dependent evars: ?14419 using ,)





destruct (IHBetaps Q H3) as (Q'' & ? & ?).
1 subgoals, subgoal 1 (ID 14656)
  
  H : forall M N P : Term,
      M →' N -> M →' P -> exists Q : Term, (N →' Q) /\ P →' Q
  M : Term
  N : Term
  P : Term
  H0 : M →' N
  H1 : N →→' P
  IHBetaps : forall N0 : Term,
             N →' N0 -> exists Q : Term, (N0 →→' Q) /\ P →' Q
  N0 : Term
  H2 : M →' N0
  Q : Term
  H3 : N →' Q
  H4 : N0 →' Q
  Q'' : Term
  H5 : Q →→' Q''
  H6 : P →' Q''
  ============================
   exists Q0 : Term, (N0 →→' Q0) /\ P →' Q0

(dependent evars: ?14419 using ,)





exists Q''; eauto.
No more subgoals.
(dependent evars: ?14419 using , ?14680 using ,)





Qed.
sub_diamond_Betaps is defined








Lemma diamond_Betaps : 

( forall M N P, M →'  N -> M →'  P -> exists Q, N →'  Q /\ P →'  Q)  ->

  forall M N P, M →→' N -> M →→' P -> exists Q, N →→' Q /\ P →→' Q .
1 subgoals, subgoal 1 (ID 14723)
  
  ============================
   (forall M N P : Term,
    M →' N -> M →' P -> exists Q : Term, (N →' Q) /\ P →' Q) ->
   forall M N P : Term,
   M →→' N -> M →→' P -> exists Q : Term, (N →→' Q) /\ P →→' Q

(dependent evars:)





intros. 
1 subgoals, subgoal 1 (ID 14729)
  
  H : forall M N P : Term,
      M →' N -> M →' P -> exists Q : Term, (N →' Q) /\ P →' Q
  M : Term
  N : Term
  P : Term
  H0 : M →→' N
  H1 : M →→' P
  ============================
   exists Q : Term, (N →→' Q) /\ P →→' Q

(dependent evars:)



revert P H1.
1 subgoals, subgoal 1 (ID 14731)
  
  H : forall M N P : Term,
      M →' N -> M →' P -> exists Q : Term, (N →' Q) /\ P →' Q
  M : Term
  N : Term
  H0 : M →→' N
  ============================
   forall P : Term, M →→' P -> exists Q : Term, (N →→' Q) /\ P →→' Q

(dependent evars:)





induction H0; intros; eauto.
1 subgoals, subgoal 1 (ID 14750)
  
  H : forall M N P : Term,
      M →' N -> M →' P -> exists Q : Term, (N →' Q) /\ P →' Q
  M : Term
  N : Term
  P : Term
  H0 : M →' N
  H1 : N →→' P
  IHBetaps : forall P0 : Term,
             N →→' P0 -> exists Q : Term, (P →→' Q) /\ P0 →→' Q
  P0 : Term
  H2 : M →→' P0
  ============================
   exists Q : Term, (P →→' Q) /\ P0 →→' Q

(dependent evars: ?14751 using ,)





destruct (sub_diamond_Betaps H M N P0 H0 H2) as (Q & ? & ?).
1 subgoals, subgoal 1 (ID 16945)
  
  H : forall M N P : Term,
      M →' N -> M →' P -> exists Q : Term, (N →' Q) /\ P →' Q
  M : Term
  N : Term
  P : Term
  H0 : M →' N
  H1 : N →→' P
  IHBetaps : forall P0 : Term,
             N →→' P0 -> exists Q : Term, (P →→' Q) /\ P0 →→' Q
  P0 : Term
  H2 : M →→' P0
  Q : Term
  H3 : N →→' Q
  H4 : P0 →' Q
  ============================
   exists Q0 : Term, (P →→' Q0) /\ P0 →→' Q0

(dependent evars: ?14751 using ,)





destruct (IHBetaps Q H3) as (Q'' & ?& ?).
1 subgoals, subgoal 1 (ID 16956)
  
  H : forall M N P : Term,
      M →' N -> M →' P -> exists Q : Term, (N →' Q) /\ P →' Q
  M : Term
  N : Term
  P : Term
  H0 : M →' N
  H1 : N →→' P
  IHBetaps : forall P0 : Term,
             N →→' P0 -> exists Q : Term, (P →→' Q) /\ P0 →→' Q
  P0 : Term
  H2 : M →→' P0
  Q : Term
  H3 : N →→' Q
  H4 : P0 →' Q
  Q'' : Term
  H5 : P →→' Q''
  H6 : Q →→' Q''
  ============================
   exists Q0 : Term, (P →→' Q0) /\ P0 →→' Q0

(dependent evars: ?14751 using ,)





exists Q'';eauto.
No more subgoals.
(dependent evars: ?14751 using , ?16988 using ,)





Qed.
diamond_Betaps is defined








Theorem Betas_diamond: 

  forall M N P, M →→ N -> M →→ P -> exists Q, N →→ Q /\ P →→ Q.
1 subgoals, subgoal 1 (ID 17026)
  
  ============================
   forall M N P : Term,
   M →→ N -> M →→ P -> exists Q : Term, (N →→ Q) /\ P →→ Q

(dependent evars:)





intros.
1 subgoals, subgoal 1 (ID 17031)
  
  M : Term
  N : Term
  P : Term
  H : M →→ N
  H0 : M →→ P
  ============================
   exists Q : Term, (N →→ Q) /\ P →→ Q

(dependent evars:)





destruct (diamond_Betaps Betap_diamond M N P) as (Q & ?& ?); intuition.
1 subgoals, subgoal 1 (ID 17048)
  
  M : Term
  N : Term
  P : Term
  H : M →→ N
  H0 : M →→ P
  Q : Term
  H1 : N →→' Q
  H2 : P →→' Q
  ============================
   exists Q0 : Term, (N →→ Q0) /\ P →→ Q0

(dependent evars:)





exists Q; intuition.
No more subgoals.
(dependent evars:)





Qed.
Betas_diamond is defined















So Beta is confluent.





Theorem Betac_confl : forall M N, M ≡ N -> exists Q, M →→ Q /\ N →→ Q.
1 subgoals, subgoal 1 (ID 17100)
  
  ============================
   forall M N : Term, M ≡ N -> exists Q : Term, (M →→ Q) /\ N →→ Q

(dependent evars:)





induction 1; eauto. 
2 subgoals, subgoal 1 (ID 17122)
  
  M : Term
  N : Term
  H : M ≡ N
  IHBetac : exists Q : Term, (M →→ Q) /\ N →→ Q
  ============================
   exists Q : Term, (N →→ Q) /\ M →→ Q

subgoal 2 (ID 17130) is:
 exists Q : Term, (M →→ Q) /\ P →→ Q
(dependent evars: ?17131 using ,)



destruct IHBetac as (Q & ? &? ); eauto.
1 subgoals, subgoal 1 (ID 17130)
  
  M : Term
  N : Term
  P : Term
  H : M ≡ N
  H0 : N ≡ P
  IHBetac1 : exists Q : Term, (M →→ Q) /\ N →→ Q
  IHBetac2 : exists Q : Term, (N →→ Q) /\ P →→ Q
  ============================
   exists Q : Term, (M →→ Q) /\ P →→ Q

(dependent evars: ?17131 using , ?17905 using ,)





destruct IHBetac1 as (Q1 & ? &? ), IHBetac2 as (Q2 & ? & ?).
1 subgoals, subgoal 1 (ID 17939)
  
  M : Term
  N : Term
  P : Term
  H : M ≡ N
  H0 : N ≡ P
  Q1 : Term
  H1 : M →→ Q1
  H2 : N →→ Q1
  Q2 : Term
  H3 : N →→ Q2
  H4 : P →→ Q2
  ============================
   exists Q : Term, (M →→ Q) /\ P →→ Q

(dependent evars: ?17131 using , ?17905 using ,)





destruct (Betas_diamond N Q1 Q2) as (Q'' & ?& ?); trivial.
1 subgoals, subgoal 1 (ID 17956)
  
  M : Term
  N : Term
  P : Term
  H : M ≡ N
  H0 : N ≡ P
  Q1 : Term
  H1 : M →→ Q1
  H2 : N →→ Q1
  Q2 : Term
  H3 : N →→ Q2
  H4 : P →→ Q2
  Q'' : Term
  H5 : Q1 →→ Q''
  H6 : Q2 →→ Q''
  ============================
   exists Q : Term, (M →→ Q) /\ P →→ Q

(dependent evars: ?17131 using , ?17905 using ,)





exists Q''; eauto.
No more subgoals.
(dependent evars: ?17131 using , ?17905 using , ?17964 using , ?18180 using ,)





Qed.
Betac_confl is defined















Some consequences:


 



    

  •  convertible sorts are equals


    • 

  •  converitble vars are equals


    • 

  •  Pi-types are Injective


    • 

  •  Pi and sorts are not convertible


    • 


 





Lemma conv_sort : forall s t, !s ≡ !t -> s = t.
1 subgoals, subgoal 1 (ID 18238)
  
  ============================
   forall s t : X.Sorts, !s ≡ !t -> s = t

(dependent evars:)





intros.
1 subgoals, subgoal 1 (ID 18241)
  
  s : X.Sorts
  t : X.Sorts
  H : !s ≡ !t
  ============================
   s = t

(dependent evars:)





apply Betac_confl in H. 
1 subgoals, subgoal 1 (ID 18243)
  
  s : X.Sorts
  t : X.Sorts
  H : exists Q : Term, (!s →→ Q) /\ !t →→ Q
  ============================
   s = t

(dependent evars:)



destruct H as (z & ?& ?).
1 subgoals, subgoal 1 (ID 18251)
  
  s : X.Sorts
  t : X.Sorts
  z : Term
  H : !s →→ z
  H0 : !t →→ z
  ============================
   s = t

(dependent evars:)





apply Betas_S in H.
1 subgoals, subgoal 1 (ID 18253)
  
  s : X.Sorts
  t : X.Sorts
  z : Term
  H : z = !s
  H0 : !t →→ z
  ============================
   s = t

(dependent evars:)





apply Betas_S in H0.
1 subgoals, subgoal 1 (ID 18255)
  
  s : X.Sorts
  t : X.Sorts
  z : Term
  H : z = !s
  H0 : z = !t
  ============================
   s = t

(dependent evars:)





rewrite H in H0.
1 subgoals, subgoal 1 (ID 18257)
  
  s : X.Sorts
  t : X.Sorts
  z : Term
  H : z = !s
  H0 : !s = !t
  ============================
   s = t

(dependent evars:)





injection H0; trivial.
No more subgoals.
(dependent evars:)





Qed.
conv_sort is defined








Lemma conv_to_sort : forall s T, !s ≡ T ->  T →→ !s.
1 subgoals, subgoal 1 (ID 18265)
  
  ============================
   forall (s : X.Sorts) (T : Term), !s ≡ T -> T →→ !s

(dependent evars:)





intros.
1 subgoals, subgoal 1 (ID 18268)
  
  s : X.Sorts
  T : Term
  H : !s ≡ T
  ============================
   T →→ !s

(dependent evars:)





apply Betac_confl in H.
1 subgoals, subgoal 1 (ID 18270)
  
  s : X.Sorts
  T : Term
  H : exists Q : Term, (!s →→ Q) /\ T →→ Q
  ============================
   T →→ !s

(dependent evars:)





destruct H as (z & ?& ?).
1 subgoals, subgoal 1 (ID 18278)
  
  s : X.Sorts
  T : Term
  z : Term
  H : !s →→ z
  H0 : T →→ z
  ============================
   T →→ !s

(dependent evars:)





apply Betas_S in H.
1 subgoals, subgoal 1 (ID 18280)
  
  s : X.Sorts
  T : Term
  z : Term
  H : z = !s
  H0 : T →→ z
  ============================
   T →→ !s

(dependent evars:)





subst. 
1 subgoals, subgoal 1 (ID 18285)
  
  s : X.Sorts
  T : Term
  H0 : T →→ !s
  ============================
   T →→ !s

(dependent evars:)



trivial.
No more subgoals.
(dependent evars:)





Qed.
conv_to_sort is defined








Lemma conv_var : forall x y, #x ≡ #y -> x = y.
1 subgoals, subgoal 1 (ID 18289)
  
  ============================
   forall x y : Vars, #x ≡ #y -> x = y

(dependent evars:)





intros.
1 subgoals, subgoal 1 (ID 18292)
  
  x : Vars
  y : Vars
  H : #x ≡ #y
  ============================
   x = y

(dependent evars:)





apply Betac_confl in H. 
1 subgoals, subgoal 1 (ID 18294)
  
  x : Vars
  y : Vars
  H : exists Q : Term, (#x →→ Q) /\ #y →→ Q
  ============================
   x = y

(dependent evars:)



destruct H as (z & ?& ?).
1 subgoals, subgoal 1 (ID 18302)
  
  x : Vars
  y : Vars
  z : Term
  H : #x →→ z
  H0 : #y →→ z
  ============================
   x = y

(dependent evars:)





apply Betas_V in H. 
1 subgoals, subgoal 1 (ID 18304)
  
  x : Vars
  y : Vars
  z : Term
  H : z = #x
  H0 : #y →→ z
  ============================
   x = y

(dependent evars:)



apply Betas_V in H0.
1 subgoals, subgoal 1 (ID 18306)
  
  x : Vars
  y : Vars
  z : Term
  H : z = #x
  H0 : z = #y
  ============================
   x = y

(dependent evars:)





rewrite H in H0.
1 subgoals, subgoal 1 (ID 18308)
  
  x : Vars
  y : Vars
  z : Term
  H : z = #x
  H0 : #x = #y
  ============================
   x = y

(dependent evars:)





injection H0; trivial.
No more subgoals.
(dependent evars:)





Qed.
conv_var is defined








Lemma conv_to_var : forall x T , #x ≡ T -> T →→ #x.
1 subgoals, subgoal 1 (ID 18316)
  
  ============================
   forall (x : Vars) (T : Term), #x ≡ T -> T →→ #x

(dependent evars:)





intros.
1 subgoals, subgoal 1 (ID 18319)
  
  x : Vars
  T : Term
  H : #x ≡ T
  ============================
   T →→ #x

(dependent evars:)





apply Betac_confl in H.
1 subgoals, subgoal 1 (ID 18321)
  
  x : Vars
  T : Term
  H : exists Q : Term, (#x →→ Q) /\ T →→ Q
  ============================
   T →→ #x

(dependent evars:)





destruct H as (z & ?& ?).
1 subgoals, subgoal 1 (ID 18329)
  
  x : Vars
  T : Term
  z : Term
  H : #x →→ z
  H0 : T →→ z
  ============================
   T →→ #x

(dependent evars:)





apply Betas_V in H.
1 subgoals, subgoal 1 (ID 18331)
  
  x : Vars
  T : Term
  z : Term
  H : z = #x
  H0 : T →→ z
  ============================
   T →→ #x

(dependent evars:)





subst; trivial.
No more subgoals.
(dependent evars:)





Qed.
conv_to_var is defined








Theorem PiInj : forall A B C D, Π(A), B ≡ Π(C), D ->  A ≡ C /\ B ≡ D.
1 subgoals, subgoal 1 (ID 18341)
  
  ============================
   forall A B C D : Term, Π (A), B ≡ Π (C), D -> (A ≡ C) /\ B ≡ D

(dependent evars:)





intros.
1 subgoals, subgoal 1 (ID 18346)
  
  A : Term
  B : Term
  C : Term
  D : Term
  H : Π (A), B ≡ Π (C), D
  ============================
   (A ≡ C) /\ B ≡ D

(dependent evars:)





apply Betac_confl in H. 
1 subgoals, subgoal 1 (ID 18348)
  
  A : Term
  B : Term
  C : Term
  D : Term
  H : exists Q : Term, (Π (A), B →→ Q) /\ Π (C), D →→ Q
  ============================
   (A ≡ C) /\ B ≡ D

(dependent evars:)



destruct H as (z & ? & ?).
1 subgoals, subgoal 1 (ID 18356)
  
  A : Term
  B : Term
  C : Term
  D : Term
  z : Term
  H : Π (A), B →→ z
  H0 : Π (C), D →→ z
  ============================
   (A ≡ C) /\ B ≡ D

(dependent evars:)





apply Betas_Pi_inv in H.
1 subgoals, subgoal 1 (ID 18358)
  
  A : Term
  B : Term
  C : Term
  D : Term
  z : Term
  H : exists C D : Term, z = Π (C), D /\ (A →→ C) /\ B →→ D
  H0 : Π (C), D →→ z
  ============================
   (A ≡ C) /\ B ≡ D

(dependent evars:)





apply Betas_Pi_inv in H0.
1 subgoals, subgoal 1 (ID 18360)
  
  A : Term
  B : Term
  C : Term
  D : Term
  z : Term
  H : exists C D : Term, z = Π (C), D /\ (A →→ C) /\ B →→ D
  H0 : exists C0 D0 : Term, z = Π (C0), D0 /\ (C →→ C0) /\ D →→ D0
  ============================
   (A ≡ C) /\ B ≡ D

(dependent evars:)





destruct H as (c1 & d1 & ? & ? & ?).
1 subgoals, subgoal 1 (ID 18381)
  
  A : Term
  B : Term
  C : Term
  D : Term
  z : Term
  c1 : Term
  d1 : Term
  H : z = Π (c1), d1
  H1 : A →→ c1
  H2 : B →→ d1
  H0 : exists C0 D0 : Term, z = Π (C0), D0 /\ (C →→ C0) /\ D →→ D0
  ============================
   (A ≡ C) /\ B ≡ D

(dependent evars:)





destruct H0 as (c2 & d2 & ? & ?& ?).
1 subgoals, subgoal 1 (ID 18397)
  
  A : Term
  B : Term
  C : Term
  D : Term
  z : Term
  c1 : Term
  d1 : Term
  H : z = Π (c1), d1
  H1 : A →→ c1
  H2 : B →→ d1
  c2 : Term
  d2 : Term
  H0 : z = Π (c2), d2
  H3 : C →→ c2
  H4 : D →→ d2
  ============================
   (A ≡ C) /\ B ≡ D

(dependent evars:)





rewrite H0 in H; injection H; intros; subst; split; eauto.
No more subgoals.
(dependent evars: ?18430 using , ?22151 using ,)





Qed.
PiInj is defined








Lemma Betac_not_Pi_sort : forall A B s, ~ (Π(A), B ≡ !s ).
1 subgoals, subgoal 1 (ID 25873)
  
  ============================
   forall (A B : Term) (s : X.Sorts), ~ (Π (A), B ≡ !s)

(dependent evars:)





intros; intro. 
1 subgoals, subgoal 1 (ID 25878)
  
  A : Term
  B : Term
  s : X.Sorts
  H : Π (A), B ≡ !s
  ============================
   False

(dependent evars:)



apply Betac_sym in H. 
1 subgoals, subgoal 1 (ID 25880)
  
  A : Term
  B : Term
  s : X.Sorts
  H : !s ≡ Π (A), B
  ============================
   False

(dependent evars:)



apply conv_to_sort in H.
1 subgoals, subgoal 1 (ID 25882)
  
  A : Term
  B : Term
  s : X.Sorts
  H : Π (A), B →→ !s
  ============================
   False

(dependent evars:)





apply Betas_Pi_inv in H as (C & D & ? & ? & ?). 
1 subgoals, subgoal 1 (ID 25900)
  
  A : Term
  B : Term
  s : X.Sorts
  C : Term
  D : Term
  H : !s = Π (C), D
  H0 : A →→ C
  H1 : B →→ D
  ============================
   False

(dependent evars:)



discriminate.
No more subgoals.
(dependent evars:)





Qed.
Betac_not_Pi_sort is defined








End ut_red_mod.
Module Type ut_red_mod is defined
















Index
This page has been generated by coqdoc