# 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[nP] N[nP] .
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 [nP] →→ 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[nP] M [nP'].
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[nP] 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[nN] →' M'[nN'].
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