Library red








Beta reduction for annotated terms 



As for the usual terms, we extend the definition of Beta to handle the
two additional annotations. Since we want to prove that the typed version
of the reduction is confluent, we don't care to prove it for this version.





Require Import Peano_dec.



Require Import Compare_dec.



Require Import Lt.



Require Import Le.



Require Import Gt.



Require Import Plus.



Require Import Minus.



Require Import Bool.



Require Import base.



Require Import term.






Module Type red_mod (X:term_sig) (TM:term_mod X).
Interactive Module Type red_mod started





Import TM.



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






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

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

 | Beta_red1 : forall M M' N A B, M → M' -> M·(A,B) N  → M'·(A,B) N

 | Beta_red2 : forall M N N' A B, N → N' -> M·(A,B) N  → M ·(A,B) N'

 | Beta_red3 : forall M N A B B', B → B' -> M·(A,B) N  → M ·(A,B') N

 | Beta_red4 : forall M N A A' B, A → A' -> M·(A,B) N  → M ·(A',B) 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) : Typ_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) : Typ_scope.
Betas is defined
Betas_ind is defined








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








Lemma Betas_App : forall M M' N N' A A' B B', M →→ M' -> N →→ N' ->  A →→ A' -> B →→ B' -> 

  M·(A,B)N →→ M'·(A',B')N'.
1 subgoals, subgoal 1 (ID 52)
  
  ============================
   forall M M' N N' A A' B B' : Term,
   M →→ M' -> N →→ N' -> A →→ A' -> B →→ B' -> M ·( A, B)N →→ M' ·( A', B')N'

(dependent evars:)





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

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





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

(dependent evars: ?100 using ,)





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

subgoal 2 (ID 118) is:
 forall M M' N N' A A' B B' : Term,
 M →→ M' -> N →→ N' -> A →→ A' -> B →→ B' -> M ·( A, B)N →→ M' ·( A', B')N'
(dependent evars: ?100 using ,)





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

(dependent evars: ?100 using , ?160 using ,)





assert (forall a b A B B', B →→ B' -> a·(A,B) b →→ a·(A,B') b).
2 subgoals, subgoal 1 (ID 182)
  
  H : forall a b c A B : Term, b →→ c -> a ·( A, B)b →→ a ·( A, B)c
  H0 : forall a b c A B : Term, b →→ c -> b ·( A, B)a →→ c ·( A, B)a
  ============================
   forall a b A B B' : Term, B →→ B' -> a ·( A, B)b →→ a ·( A, B')b

subgoal 2 (ID 183) is:
 forall M M' N N' A A' B B' : Term,
 M →→ M' -> N →→ N' -> A →→ A' -> B →→ B' -> M ·( A, B)N →→ M' ·( A', B')N'
(dependent evars: ?100 using , ?160 using ,)





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

(dependent evars: ?100 using , ?160 using , ?226 using ,)





assert (forall a b A A' B, A →→ A' -> a·(A,B) b →→ a·(A',B) b).
2 subgoals, subgoal 1 (ID 253)
  
  H : forall a b c A B : Term, b →→ c -> a ·( A, B)b →→ a ·( A, B)c
  H0 : forall a b c A B : Term, b →→ c -> b ·( A, B)a →→ c ·( A, B)a
  H1 : forall a b A B B' : Term, B →→ B' -> a ·( A, B)b →→ a ·( A, B')b
  ============================
   forall a b A A' B : Term, A →→ A' -> a ·( A, B)b →→ a ·( A', B)b

subgoal 2 (ID 254) is:
 forall M M' N N' A A' B B' : Term,
 M →→ M' -> N →→ N' -> A →→ A' -> B →→ B' -> M ·( A, B)N →→ M' ·( A', B')N'
(dependent evars: ?100 using , ?160 using , ?226 using ,)





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

(dependent evars: ?100 using , ?160 using , ?226 using , ?298 using ,)





intros. 
1 subgoals, subgoal 1 (ID 336)
  
  H : forall a b c A B : Term, b →→ c -> a ·( A, B)b →→ a ·( A, B)c
  H0 : forall a b c A B : Term, b →→ c -> b ·( A, B)a →→ c ·( A, B)a
  H1 : forall a b A B B' : Term, B →→ B' -> a ·( A, B)b →→ a ·( A, B')b
  H2 : forall a b A A' B : Term, A →→ A' -> a ·( A, B)b →→ a ·( A', B)b
  M : Term
  M' : Term
  N : Term
  N' : Term
  A : Term
  A' : Term
  B : Term
  B' : Term
  H3 : M →→ M'
  H4 : N →→ N'
  H5 : A →→ A'
  H6 : B →→ B'
  ============================
   M ·( A, B)N →→ M' ·( A', B')N'

(dependent evars: ?100 using , ?160 using , ?226 using , ?298 using ,)



eapply Betas_trans. 
2 subgoals, subgoal 1 (ID 338)
  
  H : forall a b c A B : Term, b →→ c -> a ·( A, B)b →→ a ·( A, B)c
  H0 : forall a b c A B : Term, b →→ c -> b ·( A, B)a →→ c ·( A, B)a
  H1 : forall a b A B B' : Term, B →→ B' -> a ·( A, B)b →→ a ·( A, B')b
  H2 : forall a b A A' B : Term, A →→ A' -> a ·( A, B)b →→ a ·( A', B)b
  M : Term
  M' : Term
  N : Term
  N' : Term
  A : Term
  A' : Term
  B : Term
  B' : Term
  H3 : M →→ M'
  H4 : N →→ N'
  H5 : A →→ A'
  H6 : B →→ B'
  ============================
   M ·( A, B)N →→ ?337

subgoal 2 (ID 339) is:
 ?337 →→ M' ·( A', B')N'
(dependent evars: ?100 using , ?160 using , ?226 using , ?298 using , ?337 open,)



apply H. 
2 subgoals, subgoal 1 (ID 344)
  
  H : forall a b c A B : Term, b →→ c -> a ·( A, B)b →→ a ·( A, B)c
  H0 : forall a b c A B : Term, b →→ c -> b ·( A, B)a →→ c ·( A, B)a
  H1 : forall a b A B B' : Term, B →→ B' -> a ·( A, B)b →→ a ·( A, B')b
  H2 : forall a b A A' B : Term, A →→ A' -> a ·( A, B)b →→ a ·( A', B)b
  M : Term
  M' : Term
  N : Term
  N' : Term
  A : Term
  A' : Term
  B : Term
  B' : Term
  H3 : M →→ M'
  H4 : N →→ N'
  H5 : A →→ A'
  H6 : B →→ B'
  ============================
   N →→ ?343

subgoal 2 (ID 339) is:
 M ·( A, B)?343 →→ M' ·( A', B')N'
(dependent evars: ?100 using , ?160 using , ?226 using , ?298 using , ?337 using ?343 ?342 ?341 ?340 , ?340 using , ?341 using , ?342 using , ?343 open,)



apply H4. 
1 subgoals, subgoal 1 (ID 339)
  
  H : forall a b c A B : Term, b →→ c -> a ·( A, B)b →→ a ·( A, B)c
  H0 : forall a b c A B : Term, b →→ c -> b ·( A, B)a →→ c ·( A, B)a
  H1 : forall a b A B B' : Term, B →→ B' -> a ·( A, B)b →→ a ·( A, B')b
  H2 : forall a b A A' B : Term, A →→ A' -> a ·( A, B)b →→ a ·( A', B)b
  M : Term
  M' : Term
  N : Term
  N' : Term
  A : Term
  A' : Term
  B : Term
  B' : Term
  H3 : M →→ M'
  H4 : N →→ N'
  H5 : A →→ A'
  H6 : B →→ B'
  ============================
   M ·( A, B)N' →→ M' ·( A', B')N'

(dependent evars: ?100 using , ?160 using , ?226 using , ?298 using , ?337 using ?343 ?342 ?341 ?340 , ?340 using , ?341 using , ?342 using , ?343 using ,)



eapply Betas_trans. 
2 subgoals, subgoal 1 (ID 346)
  
  H : forall a b c A B : Term, b →→ c -> a ·( A, B)b →→ a ·( A, B)c
  H0 : forall a b c A B : Term, b →→ c -> b ·( A, B)a →→ c ·( A, B)a
  H1 : forall a b A B B' : Term, B →→ B' -> a ·( A, B)b →→ a ·( A, B')b
  H2 : forall a b A A' B : Term, A →→ A' -> a ·( A, B)b →→ a ·( A', B)b
  M : Term
  M' : Term
  N : Term
  N' : Term
  A : Term
  A' : Term
  B : Term
  B' : Term
  H3 : M →→ M'
  H4 : N →→ N'
  H5 : A →→ A'
  H6 : B →→ B'
  ============================
   M ·( A, B)N' →→ ?345

subgoal 2 (ID 347) is:
 ?345 →→ M' ·( A', B')N'
(dependent evars: ?100 using , ?160 using , ?226 using , ?298 using , ?337 using ?343 ?342 ?341 ?340 , ?340 using , ?341 using , ?342 using , ?343 using , ?345 open,)



apply H0. 
2 subgoals, subgoal 1 (ID 352)
  
  H : forall a b c A B : Term, b →→ c -> a ·( A, B)b →→ a ·( A, B)c
  H0 : forall a b c A B : Term, b →→ c -> b ·( A, B)a →→ c ·( A, B)a
  H1 : forall a b A B B' : Term, B →→ B' -> a ·( A, B)b →→ a ·( A, B')b
  H2 : forall a b A A' B : Term, A →→ A' -> a ·( A, B)b →→ a ·( A', B)b
  M : Term
  M' : Term
  N : Term
  N' : Term
  A : Term
  A' : Term
  B : Term
  B' : Term
  H3 : M →→ M'
  H4 : N →→ N'
  H5 : A →→ A'
  H6 : B →→ B'
  ============================
   M →→ ?348

subgoal 2 (ID 347) is:
 ?348 ·( A, B)N' →→ M' ·( A', B')N'
(dependent evars: ?100 using , ?160 using , ?226 using , ?298 using , ?337 using ?343 ?342 ?341 ?340 , ?340 using , ?341 using , ?342 using , ?343 using , ?345 using ?351 ?350 ?349 ?348 , ?348 open, ?349 using , ?350 using , ?351 using ,)



apply H3. 
1 subgoals, subgoal 1 (ID 347)
  
  H : forall a b c A B : Term, b →→ c -> a ·( A, B)b →→ a ·( A, B)c
  H0 : forall a b c A B : Term, b →→ c -> b ·( A, B)a →→ c ·( A, B)a
  H1 : forall a b A B B' : Term, B →→ B' -> a ·( A, B)b →→ a ·( A, B')b
  H2 : forall a b A A' B : Term, A →→ A' -> a ·( A, B)b →→ a ·( A', B)b
  M : Term
  M' : Term
  N : Term
  N' : Term
  A : Term
  A' : Term
  B : Term
  B' : Term
  H3 : M →→ M'
  H4 : N →→ N'
  H5 : A →→ A'
  H6 : B →→ B'
  ============================
   M' ·( A, B)N' →→ M' ·( A', B')N'

(dependent evars: ?100 using , ?160 using , ?226 using , ?298 using , ?337 using ?343 ?342 ?341 ?340 , ?340 using , ?341 using , ?342 using , ?343 using , ?345 using ?351 ?350 ?349 ?348 , ?348 using , ?349 using , ?350 using , ?351 using ,)



eauto.
No more subgoals.
(dependent evars: ?100 using , ?160 using , ?226 using , ?298 using , ?337 using ?343 ?342 ?341 ?340 , ?340 using , ?341 using , ?342 using , ?343 using , ?345 using ?351 ?350 ?349 ?348 , ?348 using , ?349 using , ?350 using , ?351 using , ?354 using , ?382 using ?398 ?397 ?396 ?395 , ?395 using , ?396 using , ?397 using , ?398 using ,)





Qed.
Betas_App is defined








Hint Resolve Betas_App.






Lemma Betas_La : forall A A' M M', A →→ A' -> M →→ M' -> λ[A],M →→ λ[A'],M'.
1 subgoals, subgoal 1 (ID 696)
  
  ============================
   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 700)
  
  ============================
   forall a b c : Term, a →→ b -> λ [c], a →→ λ [c], b

subgoal 2 (ID 701) 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 701)
  
  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: ?740 using ,)





assert (forall a b c, a →→ b -> λ[a], c →→ λ[b], c).
2 subgoals, subgoal 1 (ID 755)
  
  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 756) is:
 forall A A' M M' : Term, A →→ A' -> M →→ M' -> λ [A], M →→ λ [A'], M'
(dependent evars: ?740 using ,)





induction 1; eauto.
1 subgoals, subgoal 1 (ID 756)
  
  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: ?740 using , ?796 using ,)





eauto.
No more subgoals.
(dependent evars: ?740 using , ?796 using , ?818 using , ?832 using ?836 ?835 , ?835 using , ?836 using ,)





Qed.
Betas_La is defined








Hint Resolve Betas_La.






Lemma Betas_Pi : forall A A' B B', A →→ A' -> B →→ B' -> Π(A),B →→ Π(A'),B'.
1 subgoals, subgoal 1 (ID 950)
  
  ============================
   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 954)
  
  ============================
   forall a b c : Term, a →→ b -> Π (c), a →→ Π (c), b

subgoal 2 (ID 955) 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 955)
  
  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: ?994 using ,)





assert (forall a b c, a →→ b -> Π(a), c →→ Π(b), c).
2 subgoals, subgoal 1 (ID 1009)
  
  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 1010) is:
 forall A A' B B' : Term, A →→ A' -> B →→ B' -> Π (A), B →→ Π (A'), B'
(dependent evars: ?994 using ,)





induction 1; eauto.
1 subgoals, subgoal 1 (ID 1010)
  
  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: ?994 using , ?1050 using ,)





eauto.
No more subgoals.
(dependent evars: ?994 using , ?1050 using , ?1072 using , ?1086 using ?1090 ?1089 , ?1089 using , ?1090 using ,)





Qed.
Betas_Pi is defined








Hint Resolve Betas_Pi.






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






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

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

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

 | 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' A A' B B', M →' M' -> N →' N' -> A →' A' -> B →' B' ->

    M ·(A,B) N →' M'·(A',B') N'

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

where "A →' B" := (Betap A B ) : Typ_scope.
Betap is defined
Betap_ind is defined








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






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

 | Betaps_intro : forall M N  , M →'  N -> M →→' N

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

where "M →→' N" := (Betaps M N) : Typ_scope.
Betaps is defined
Betaps_ind is defined








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








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

(dependent evars:)





induction 1; intuition.
1 subgoals, subgoal 1 (ID 1310)
  
  A : Term
  M : Term
  M' : Term
  N : Term
  N' : Term
  K : Term
  L : Term
  H : M →' M'
  H0 : N →' N'
  IHBetap1 : M →→ M'
  IHBetap2 : N →→ N'
  ============================
   (λ [A], M) ·( K, L)N →→ M' [ ← N']

(dependent evars:)





eapply Betas_trans. 
2 subgoals, subgoal 1 (ID 1376)
  
  A : Term
  M : Term
  M' : Term
  N : Term
  N' : Term
  K : Term
  L : Term
  H : M →' M'
  H0 : N →' N'
  IHBetap1 : M →→ M'
  IHBetap2 : N →→ N'
  ============================
   (λ [A], M) ·( K, L)N →→ ?1375

subgoal 2 (ID 1377) is:
 ?1375 →→ M' [ ← N']
(dependent evars: ?1375 open,)



eapply Betas_App. 
5 subgoals, subgoal 1 (ID 1382)
  
  A : Term
  M : Term
  M' : Term
  N : Term
  N' : Term
  K : Term
  L : Term
  H : M →' M'
  H0 : N →' N'
  IHBetap1 : M →→ M'
  IHBetap2 : N →→ N'
  ============================
   λ [A], M →→ ?1378

subgoal 2 (ID 1383) is:
 N →→ ?1381
subgoal 3 (ID 1384) is:
 K →→ ?1379
subgoal 4 (ID 1385) is:
 L →→ ?1380
subgoal 5 (ID 1377) is:
 ?1378 ·( ?1379, ?1380)?1381 →→ M' [ ← N']
(dependent evars: ?1375 using ?1381 ?1380 ?1379 ?1378 , ?1378 open, ?1379 open, ?1380 open, ?1381 open,)



eapply Betas_La. 
6 subgoals, subgoal 1 (ID 1388)
  
  A : Term
  M : Term
  M' : Term
  N : Term
  N' : Term
  K : Term
  L : Term
  H : M →' M'
  H0 : N →' N'
  IHBetap1 : M →→ M'
  IHBetap2 : N →→ N'
  ============================
   A →→ ?1386

subgoal 2 (ID 1389) is:
 M →→ ?1387
subgoal 3 (ID 1383) is:
 N →→ ?1381
subgoal 4 (ID 1384) is:
 K →→ ?1379
subgoal 5 (ID 1385) is:
 L →→ ?1380
subgoal 6 (ID 1377) is:
 (λ [?1386], ?1387) ·( ?1379, ?1380)?1381 →→ M' [ ← N']
(dependent evars: ?1375 using ?1381 ?1380 ?1379 ?1378 , ?1378 using ?1387 ?1386 , ?1379 open, ?1380 open, ?1381 open, ?1386 open, ?1387 open,)



apply Betas_refl.
5 subgoals, subgoal 1 (ID 1389)
  
  A : Term
  M : Term
  M' : Term
  N : Term
  N' : Term
  K : Term
  L : Term
  H : M →' M'
  H0 : N →' N'
  IHBetap1 : M →→ M'
  IHBetap2 : N →→ N'
  ============================
   M →→ ?1387

subgoal 2 (ID 1383) is:
 N →→ ?1381
subgoal 3 (ID 1384) is:
 K →→ ?1379
subgoal 4 (ID 1385) is:
 L →→ ?1380
subgoal 5 (ID 1377) is:
 (λ [A], ?1387) ·( ?1379, ?1380)?1381 →→ M' [ ← N']
(dependent evars: ?1375 using ?1381 ?1380 ?1379 ?1378 , ?1378 using ?1387 ?1386 , ?1379 open, ?1380 open, ?1381 open, ?1386 using , ?1387 open,)





apply IHBetap1. 
4 subgoals, subgoal 1 (ID 1383)
  
  A : Term
  M : Term
  M' : Term
  N : Term
  N' : Term
  K : Term
  L : Term
  H : M →' M'
  H0 : N →' N'
  IHBetap1 : M →→ M'
  IHBetap2 : N →→ N'
  ============================
   N →→ ?1381

subgoal 2 (ID 1384) is:
 K →→ ?1379
subgoal 3 (ID 1385) is:
 L →→ ?1380
subgoal 4 (ID 1377) is:
 (λ [A], M') ·( ?1379, ?1380)?1381 →→ M' [ ← N']
(dependent evars: ?1375 using ?1381 ?1380 ?1379 ?1378 , ?1378 using ?1387 ?1386 , ?1379 open, ?1380 open, ?1381 open, ?1386 using , ?1387 using ,)



apply IHBetap2. 
3 subgoals, subgoal 1 (ID 1384)
  
  A : Term
  M : Term
  M' : Term
  N : Term
  N' : Term
  K : Term
  L : Term
  H : M →' M'
  H0 : N →' N'
  IHBetap1 : M →→ M'
  IHBetap2 : N →→ N'
  ============================
   K →→ ?1379

subgoal 2 (ID 1385) is:
 L →→ ?1380
subgoal 3 (ID 1377) is:
 (λ [A], M') ·( ?1379, ?1380)N' →→ M' [ ← N']
(dependent evars: ?1375 using ?1381 ?1380 ?1379 ?1378 , ?1378 using ?1387 ?1386 , ?1379 open, ?1380 open, ?1381 using , ?1386 using , ?1387 using ,)



apply Betas_refl. 
2 subgoals, subgoal 1 (ID 1385)
  
  A : Term
  M : Term
  M' : Term
  N : Term
  N' : Term
  K : Term
  L : Term
  H : M →' M'
  H0 : N →' N'
  IHBetap1 : M →→ M'
  IHBetap2 : N →→ N'
  ============================
   L →→ ?1380

subgoal 2 (ID 1377) is:
 (λ [A], M') ·( K, ?1380)N' →→ M' [ ← N']
(dependent evars: ?1375 using ?1381 ?1380 ?1379 ?1378 , ?1378 using ?1387 ?1386 , ?1379 using , ?1380 open, ?1381 using , ?1386 using , ?1387 using ,)



apply Betas_refl.
1 subgoals, subgoal 1 (ID 1377)
  
  A : Term
  M : Term
  M' : Term
  N : Term
  N' : Term
  K : Term
  L : Term
  H : M →' M'
  H0 : N →' N'
  IHBetap1 : M →→ M'
  IHBetap2 : N →→ N'
  ============================
   (λ [A], M') ·( K, L)N' →→ M' [ ← N']

(dependent evars: ?1375 using ?1381 ?1380 ?1379 ?1378 , ?1378 using ?1387 ?1386 , ?1379 using , ?1380 using , ?1381 using , ?1386 using , ?1387 using ,)





constructor. 
1 subgoals, subgoal 1 (ID 1392)
  
  A : Term
  M : Term
  M' : Term
  N : Term
  N' : Term
  K : Term
  L : Term
  H : M →' M'
  H0 : N →' N'
  IHBetap1 : M →→ M'
  IHBetap2 : N →→ N'
  ============================
   (λ [A], M') ·( K, L)N' → M' [ ← N']

(dependent evars: ?1375 using ?1381 ?1380 ?1379 ?1378 , ?1378 using ?1387 ?1386 , ?1379 using , ?1380 using , ?1381 using , ?1386 using , ?1387 using ,)



econstructor.
No more subgoals.
(dependent evars: ?1375 using ?1381 ?1380 ?1379 ?1378 , ?1378 using ?1387 ?1386 , ?1379 using , ?1380 using , ?1381 using , ?1386 using , ?1387 using ,)





Qed.
Betap_to_Betas is defined








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

(dependent evars:)





induction 1; eauto. 
1 subgoals, subgoal 1 (ID 1410)
  
  M : Term
  N : Term
  H : M →' N
  ============================
   M →→ N

(dependent evars: ?1676 using ,)



apply Betap_to_Betas in H; trivial.
No more subgoals.
(dependent evars: ?1676 using ,)





Qed.
Betaps_to_Betas is defined








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

(dependent evars:)





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





Qed.
Betap_refl is defined








Hint Resolve Betap_refl.






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

(dependent evars:)





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





Qed.
Betaps_Beta_closure is defined








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

(dependent evars:)





induction 1. 
3 subgoals, subgoal 1 (ID 1957)
  
  M : Term
  ============================
   M →→' M

subgoal 2 (ID 1960) is:
 M →→' N
subgoal 3 (ID 1968) is:
 M →→' P
(dependent evars:)



intuition.
2 subgoals, subgoal 1 (ID 1960)
  
  M : Term
  N : Term
  H : M → N
  ============================
   M →→' N

subgoal 2 (ID 1968) is:
 M →→' P
(dependent evars:)





apply Betaps_Beta_closure in  H; intuition.
1 subgoals, subgoal 1 (ID 1968)
  
  M : Term
  N : Term
  P : Term
  H : M →→ N
  H0 : N →→ P
  IHBetas1 : M →→' N
  IHBetas2 : N →→' P
  ============================
   M →→' P

(dependent evars:)





eauto.
No more subgoals.
(dependent evars: ?1980 using ,)





Qed.
Betaps_Betas_closure is defined








End red_mod.
Module Type red_mod is defined
















Index
This page has been generated by coqdoc