In order to prove SR, we need to be able to talk
about reduction inside a context.
Some basic properties of Beta inside context.
There is two ways to prove SR: either we prove that reduction inside the
context and inside the term "at the same time" is valid, or we first do this
for the context only at first, but we need to weaken a little the hypothesis.
Here we choose the second solution. First step toward full SR: if we do reductions inside the context
of a valid judgment, and if the resulting context is well-formed,
then the judgement is still valid with the resulting context.
Lemma Beta_env_sound : forall Γ M T, Γ ⊢ M : T -> forall Γ', Γ' ⊣ -> Γ →e Γ' -> Γ' ⊢ M : T .1 subgoals, subgoal 1 (ID 798)
============================
forall (Γ : Env) (M T : Term),
Γ ⊢ M : T -> forall Γ' : Env, Γ' ⊣ -> Γ →e Γ' -> Γ' ⊢ M : T
(dependent evars:)
induction 1; intros.6 subgoals, subgoal 1 (ID 894)
Γ : Env
s : X.Sorts
t : X.Sorts
H : Y.Ax s t
H0 : Γ ⊣
Γ' : Env
H1 : Γ' ⊣
H2 : Γ →e Γ'
============================
Γ' ⊢ !s : !t
subgoal 2 (ID 897) is:
Γ' ⊢ #v : A
subgoal 3 (ID 900) is:
Γ' ⊢ Π (A), B : !u
subgoal 4 (ID 903) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 5 (ID 906) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 6 (ID 909) is:
Γ' ⊢ M : B
(dependent evars:)
constructor; trivial.5 subgoals, subgoal 1 (ID 897)
Γ : Env
A : Term
v : nat
H : Γ ⊣
H0 : A ↓ v ⊂ Γ
Γ' : Env
H1 : Γ' ⊣
H2 : Γ →e Γ'
============================
Γ' ⊢ #v : A
subgoal 2 (ID 900) is:
Γ' ⊢ Π (A), B : !u
subgoal 3 (ID 903) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 4 (ID 906) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 5 (ID 909) is:
Γ' ⊢ M : B
(dependent evars:)
revert A v H0 H H1.5 subgoals, subgoal 1 (ID 914)
Γ : Env
Γ' : Env
H2 : Γ →e Γ'
============================
forall (A : Term) (v : nat), A ↓ v ⊂ Γ -> Γ ⊣ -> Γ' ⊣ -> Γ' ⊢ #v : A
subgoal 2 (ID 900) is:
Γ' ⊢ Π (A), B : !u
subgoal 3 (ID 903) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 4 (ID 906) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 5 (ID 909) is:
Γ' ⊢ M : B
(dependent evars:)
induction H2; intros. 6 subgoals, subgoal 1 (ID 936)
A : Term
B : Term
Γ : list Term
H : A → B
A0 : Term
v : nat
H0 : A0 ↓ v ⊂ A :: Γ
H1 : A :: Γ ⊣
H2 : B :: Γ ⊣
============================
B :: Γ ⊢ #v : A0
subgoal 2 (ID 941) is:
A :: Γ' ⊢ #v : A0
subgoal 3 (ID 900) is:
Γ' ⊢ Π (A), B : !u
subgoal 4 (ID 903) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 5 (ID 906) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 6 (ID 909) is:
Γ' ⊢ M : B
(dependent evars:)
destruct H0 as (AA& ? & ?). 6 subgoals, subgoal 1 (ID 952)
A : Term
B : Term
Γ : list Term
H : A → B
A0 : Term
v : nat
AA : Term
H0 : A0 = AA ↑ (S v)
H3 : AA ↓ v ∈ A :: Γ
H1 : A :: Γ ⊣
H2 : B :: Γ ⊣
============================
B :: Γ ⊢ #v : A0
subgoal 2 (ID 941) is:
A :: Γ' ⊢ #v : A0
subgoal 3 (ID 900) is:
Γ' ⊢ Π (A), B : !u
subgoal 4 (ID 903) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 5 (ID 906) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 6 (ID 909) is:
Γ' ⊢ M : B
(dependent evars:)
inversion H3; subst; clear H3.7 subgoals, subgoal 1 (ID 1041)
A : Term
B : Term
Γ : list Term
H : A → B
H1 : A :: Γ ⊣
H2 : B :: Γ ⊣
============================
B :: Γ ⊢ #0 : A ↑ 1
subgoal 2 (ID 1042) is:
B :: Γ ⊢ #(S n) : AA ↑ (S (S n))
subgoal 3 (ID 941) is:
A :: Γ' ⊢ #v : A0
subgoal 4 (ID 900) is:
Γ' ⊢ Π (A), B : !u
subgoal 5 (ID 903) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 6 (ID 906) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 7 (ID 909) is:
Γ' ⊢ M : B
(dependent evars:)
inversion H1; subst; clear H1. 7 subgoals, subgoal 1 (ID 1091)
A : Term
B : Term
Γ : list Term
H : A → B
H2 : B :: Γ ⊣
s : X.Sorts
H3 : Γ ⊢ A : !s
============================
B :: Γ ⊢ #0 : A ↑ 1
subgoal 2 (ID 1042) is:
B :: Γ ⊢ #(S n) : AA ↑ (S (S n))
subgoal 3 (ID 941) is:
A :: Γ' ⊢ #v : A0
subgoal 4 (ID 900) is:
Γ' ⊢ Π (A), B : !u
subgoal 5 (ID 903) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 6 (ID 906) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 7 (ID 909) is:
Γ' ⊢ M : B
(dependent evars:)
inversion H2; subst; clear H2.7 subgoals, subgoal 1 (ID 1140)
A : Term
B : Term
Γ : list Term
H : A → B
s : X.Sorts
H3 : Γ ⊢ A : !s
s0 : X.Sorts
H1 : Γ ⊢ B : !s0
============================
B :: Γ ⊢ #0 : A ↑ 1
subgoal 2 (ID 1042) is:
B :: Γ ⊢ #(S n) : AA ↑ (S (S n))
subgoal 3 (ID 941) is:
A :: Γ' ⊢ #v : A0
subgoal 4 (ID 900) is:
Γ' ⊢ Π (A), B : !u
subgoal 5 (ID 903) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 6 (ID 906) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 7 (ID 909) is:
Γ' ⊢ M : B
(dependent evars:)
apply Cnv with ( B ↑ 1 ) s. 9 subgoals, subgoal 1 (ID 1141)
A : Term
B : Term
Γ : list Term
H : A → B
s : X.Sorts
H3 : Γ ⊢ A : !s
s0 : X.Sorts
H1 : Γ ⊢ B : !s0
============================
B ↑ 1 ≡ A ↑ 1
subgoal 2 (ID 1142) is:
B :: Γ ⊢ #0 : B ↑ 1
subgoal 3 (ID 1143) is:
B :: Γ ⊢ A ↑ 1 : !s
subgoal 4 (ID 1042) is:
B :: Γ ⊢ #(S n) : AA ↑ (S (S n))
subgoal 5 (ID 941) is:
A :: Γ' ⊢ #v : A0
subgoal 6 (ID 900) is:
Γ' ⊢ Π (A), B : !u
subgoal 7 (ID 903) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 8 (ID 906) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 9 (ID 909) is:
Γ' ⊢ M : B
(dependent evars:)
intuition.8 subgoals, subgoal 1 (ID 1142)
A : Term
B : Term
Γ : list Term
H : A → B
s : X.Sorts
H3 : Γ ⊢ A : !s
s0 : X.Sorts
H1 : Γ ⊢ B : !s0
============================
B :: Γ ⊢ #0 : B ↑ 1
subgoal 2 (ID 1143) is:
B :: Γ ⊢ A ↑ 1 : !s
subgoal 3 (ID 1042) is:
B :: Γ ⊢ #(S n) : AA ↑ (S (S n))
subgoal 4 (ID 941) is:
A :: Γ' ⊢ #v : A0
subgoal 5 (ID 900) is:
Γ' ⊢ Π (A), B : !u
subgoal 6 (ID 903) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 7 (ID 906) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 8 (ID 909) is:
Γ' ⊢ M : B
(dependent evars:)
constructor. 9 subgoals, subgoal 1 (ID 1165)
A : Term
B : Term
Γ : list Term
H : A → B
s : X.Sorts
H3 : Γ ⊢ A : !s
s0 : X.Sorts
H1 : Γ ⊢ B : !s0
============================
B :: Γ ⊣
subgoal 2 (ID 1166) is:
B ↑ 1 ↓ 0 ⊂ B :: Γ
subgoal 3 (ID 1143) is:
B :: Γ ⊢ A ↑ 1 : !s
subgoal 4 (ID 1042) is:
B :: Γ ⊢ #(S n) : AA ↑ (S (S n))
subgoal 5 (ID 941) is:
A :: Γ' ⊢ #v : A0
subgoal 6 (ID 900) is:
Γ' ⊢ Π (A), B : !u
subgoal 7 (ID 903) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 8 (ID 906) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 9 (ID 909) is:
Γ' ⊢ M : B
(dependent evars:)
econstructor;apply H1. 8 subgoals, subgoal 1 (ID 1166)
A : Term
B : Term
Γ : list Term
H : A → B
s : X.Sorts
H3 : Γ ⊢ A : !s
s0 : X.Sorts
H1 : Γ ⊢ B : !s0
============================
B ↑ 1 ↓ 0 ⊂ B :: Γ
subgoal 2 (ID 1143) is:
B :: Γ ⊢ A ↑ 1 : !s
subgoal 3 (ID 1042) is:
B :: Γ ⊢ #(S n) : AA ↑ (S (S n))
subgoal 4 (ID 941) is:
A :: Γ' ⊢ #v : A0
subgoal 5 (ID 900) is:
Γ' ⊢ Π (A), B : !u
subgoal 6 (ID 903) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 7 (ID 906) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 8 (ID 909) is:
Γ' ⊢ M : B
(dependent evars: ?1169 using ,)
exists B; intuition.7 subgoals, subgoal 1 (ID 1143)
A : Term
B : Term
Γ : list Term
H : A → B
s : X.Sorts
H3 : Γ ⊢ A : !s
s0 : X.Sorts
H1 : Γ ⊢ B : !s0
============================
B :: Γ ⊢ A ↑ 1 : !s
subgoal 2 (ID 1042) is:
B :: Γ ⊢ #(S n) : AA ↑ (S (S n))
subgoal 3 (ID 941) is:
A :: Γ' ⊢ #v : A0
subgoal 4 (ID 900) is:
Γ' ⊢ Π (A), B : !u
subgoal 5 (ID 903) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 6 (ID 906) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 7 (ID 909) is:
Γ' ⊢ M : B
(dependent evars: ?1169 using ,)
change !s with !s ↑ 1. 7 subgoals, subgoal 1 (ID 1187)
A : Term
B : Term
Γ : list Term
H : A → B
s : X.Sorts
H3 : Γ ⊢ A : !s
s0 : X.Sorts
H1 : Γ ⊢ B : !s0
============================
B :: Γ ⊢ A ↑ 1 : !s ↑ 1
subgoal 2 (ID 1042) is:
B :: Γ ⊢ #(S n) : AA ↑ (S (S n))
subgoal 3 (ID 941) is:
A :: Γ' ⊢ #v : A0
subgoal 4 (ID 900) is:
Γ' ⊢ Π (A), B : !u
subgoal 5 (ID 903) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 6 (ID 906) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 7 (ID 909) is:
Γ' ⊢ M : B
(dependent evars: ?1169 using ,)
apply thinning with s0 ;trivial.6 subgoals, subgoal 1 (ID 1042)
A : Term
B : Term
Γ : list Term
H : A → B
AA : Term
H1 : A :: Γ ⊣
H2 : B :: Γ ⊣
n : nat
H7 : AA ↓ n ∈ Γ
============================
B :: Γ ⊢ #(S n) : AA ↑ (S (S n))
subgoal 2 (ID 941) is:
A :: Γ' ⊢ #v : A0
subgoal 3 (ID 900) is:
Γ' ⊢ Π (A), B : !u
subgoal 4 (ID 903) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 5 (ID 906) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 6 (ID 909) is:
Γ' ⊢ M : B
(dependent evars: ?1169 using ,)
constructor. 7 subgoals, subgoal 1 (ID 1192)
A : Term
B : Term
Γ : list Term
H : A → B
AA : Term
H1 : A :: Γ ⊣
H2 : B :: Γ ⊣
n : nat
H7 : AA ↓ n ∈ Γ
============================
B :: Γ ⊣
subgoal 2 (ID 1193) is:
AA ↑ (S (S n)) ↓ S n ⊂ B :: Γ
subgoal 3 (ID 941) is:
A :: Γ' ⊢ #v : A0
subgoal 4 (ID 900) is:
Γ' ⊢ Π (A), B : !u
subgoal 5 (ID 903) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 6 (ID 906) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 7 (ID 909) is:
Γ' ⊢ M : B
(dependent evars: ?1169 using ,)
trivial. 6 subgoals, subgoal 1 (ID 1193)
A : Term
B : Term
Γ : list Term
H : A → B
AA : Term
H1 : A :: Γ ⊣
H2 : B :: Γ ⊣
n : nat
H7 : AA ↓ n ∈ Γ
============================
AA ↑ (S (S n)) ↓ S n ⊂ B :: Γ
subgoal 2 (ID 941) is:
A :: Γ' ⊢ #v : A0
subgoal 3 (ID 900) is:
Γ' ⊢ Π (A), B : !u
subgoal 4 (ID 903) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 5 (ID 906) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 6 (ID 909) is:
Γ' ⊢ M : B
(dependent evars: ?1169 using ,)
exists AA; intuition.5 subgoals, subgoal 1 (ID 941)
A : Term
Γ : Env
Γ' : Env
H2 : Γ →e Γ'
IHBeta_env : forall (A : Term) (v : nat),
A ↓ v ⊂ Γ -> Γ ⊣ -> Γ' ⊣ -> Γ' ⊢ #v : A
A0 : Term
v : nat
H0 : A0 ↓ v ⊂ A :: Γ
H : A :: Γ ⊣
H1 : A :: Γ' ⊣
============================
A :: Γ' ⊢ #v : A0
subgoal 2 (ID 900) is:
Γ' ⊢ Π (A), B : !u
subgoal 3 (ID 903) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 4 (ID 906) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 5 (ID 909) is:
Γ' ⊢ M : B
(dependent evars: ?1169 using ,)
destruct H0 as (AA& ? & ?). 5 subgoals, subgoal 1 (ID 1221)
A : Term
Γ : Env
Γ' : Env
H2 : Γ →e Γ'
IHBeta_env : forall (A : Term) (v : nat),
A ↓ v ⊂ Γ -> Γ ⊣ -> Γ' ⊣ -> Γ' ⊢ #v : A
A0 : Term
v : nat
AA : Term
H0 : A0 = AA ↑ (S v)
H3 : AA ↓ v ∈ A :: Γ
H : A :: Γ ⊣
H1 : A :: Γ' ⊣
============================
A :: Γ' ⊢ #v : A0
subgoal 2 (ID 900) is:
Γ' ⊢ Π (A), B : !u
subgoal 3 (ID 903) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 4 (ID 906) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 5 (ID 909) is:
Γ' ⊢ M : B
(dependent evars: ?1169 using ,)
inversion H3; subst; clear H3.6 subgoals, subgoal 1 (ID 1310)
A : Term
Γ : Env
Γ' : Env
H2 : Γ →e Γ'
IHBeta_env : forall (A : Term) (v : nat),
A ↓ v ⊂ Γ -> Γ ⊣ -> Γ' ⊣ -> Γ' ⊢ #v : A
H : A :: Γ ⊣
H1 : A :: Γ' ⊣
============================
A :: Γ' ⊢ #0 : A ↑ 1
subgoal 2 (ID 1311) is:
A :: Γ' ⊢ #(S n) : AA ↑ (S (S n))
subgoal 3 (ID 900) is:
Γ' ⊢ Π (A), B : !u
subgoal 4 (ID 903) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 5 (ID 906) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 6 (ID 909) is:
Γ' ⊢ M : B
(dependent evars: ?1169 using ,)
constructor. 7 subgoals, subgoal 1 (ID 1314)
A : Term
Γ : Env
Γ' : Env
H2 : Γ →e Γ'
IHBeta_env : forall (A : Term) (v : nat),
A ↓ v ⊂ Γ -> Γ ⊣ -> Γ' ⊣ -> Γ' ⊢ #v : A
H : A :: Γ ⊣
H1 : A :: Γ' ⊣
============================
A :: Γ' ⊣
subgoal 2 (ID 1315) is:
A ↑ 1 ↓ 0 ⊂ A :: Γ'
subgoal 3 (ID 1311) is:
A :: Γ' ⊢ #(S n) : AA ↑ (S (S n))
subgoal 4 (ID 900) is:
Γ' ⊢ Π (A), B : !u
subgoal 5 (ID 903) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 6 (ID 906) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 7 (ID 909) is:
Γ' ⊢ M : B
(dependent evars: ?1169 using ,)
trivial. 6 subgoals, subgoal 1 (ID 1315)
A : Term
Γ : Env
Γ' : Env
H2 : Γ →e Γ'
IHBeta_env : forall (A : Term) (v : nat),
A ↓ v ⊂ Γ -> Γ ⊣ -> Γ' ⊣ -> Γ' ⊢ #v : A
H : A :: Γ ⊣
H1 : A :: Γ' ⊣
============================
A ↑ 1 ↓ 0 ⊂ A :: Γ'
subgoal 2 (ID 1311) is:
A :: Γ' ⊢ #(S n) : AA ↑ (S (S n))
subgoal 3 (ID 900) is:
Γ' ⊢ Π (A), B : !u
subgoal 4 (ID 903) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 5 (ID 906) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 6 (ID 909) is:
Γ' ⊢ M : B
(dependent evars: ?1169 using ,)
exists A; intuition.5 subgoals, subgoal 1 (ID 1311)
A : Term
Γ : Env
Γ' : Env
H2 : Γ →e Γ'
IHBeta_env : forall (A : Term) (v : nat),
A ↓ v ⊂ Γ -> Γ ⊣ -> Γ' ⊣ -> Γ' ⊢ #v : A
AA : Term
H : A :: Γ ⊣
H1 : A :: Γ' ⊣
n : nat
H7 : AA ↓ n ∈ Γ
============================
A :: Γ' ⊢ #(S n) : AA ↑ (S (S n))
subgoal 2 (ID 900) is:
Γ' ⊢ Π (A), B : !u
subgoal 3 (ID 903) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 4 (ID 906) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 5 (ID 909) is:
Γ' ⊢ M : B
(dependent evars: ?1169 using ,)
change (S(S n)) with (1+S n). 5 subgoals, subgoal 1 (ID 1331)
A : Term
Γ : Env
Γ' : Env
H2 : Γ →e Γ'
IHBeta_env : forall (A : Term) (v : nat),
A ↓ v ⊂ Γ -> Γ ⊣ -> Γ' ⊣ -> Γ' ⊢ #v : A
AA : Term
H : A :: Γ ⊣
H1 : A :: Γ' ⊣
n : nat
H7 : AA ↓ n ∈ Γ
============================
A :: Γ' ⊢ #(S n) : AA ↑ (1 + S n)
subgoal 2 (ID 900) is:
Γ' ⊢ Π (A), B : !u
subgoal 3 (ID 903) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 4 (ID 906) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 5 (ID 909) is:
Γ' ⊢ M : B
(dependent evars: ?1169 using ,)
change #(S n) with (#n ↑ 1).5 subgoals, subgoal 1 (ID 1333)
A : Term
Γ : Env
Γ' : Env
H2 : Γ →e Γ'
IHBeta_env : forall (A : Term) (v : nat),
A ↓ v ⊂ Γ -> Γ ⊣ -> Γ' ⊣ -> Γ' ⊢ #v : A
AA : Term
H : A :: Γ ⊣
H1 : A :: Γ' ⊣
n : nat
H7 : AA ↓ n ∈ Γ
============================
A :: Γ' ⊢ #n ↑ 1 : AA ↑ (1 + S n)
subgoal 2 (ID 900) is:
Γ' ⊢ Π (A), B : !u
subgoal 3 (ID 903) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 4 (ID 906) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 5 (ID 909) is:
Γ' ⊢ M : B
(dependent evars: ?1169 using ,)
rewrite <- lift_lift.5 subgoals, subgoal 1 (ID 1334)
A : Term
Γ : Env
Γ' : Env
H2 : Γ →e Γ'
IHBeta_env : forall (A : Term) (v : nat),
A ↓ v ⊂ Γ -> Γ ⊣ -> Γ' ⊣ -> Γ' ⊢ #v : A
AA : Term
H : A :: Γ ⊣
H1 : A :: Γ' ⊣
n : nat
H7 : AA ↓ n ∈ Γ
============================
A :: Γ' ⊢ #n ↑ 1 : AA ↑ (S n) ↑ 1
subgoal 2 (ID 900) is:
Γ' ⊢ Π (A), B : !u
subgoal 3 (ID 903) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 4 (ID 906) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 5 (ID 909) is:
Γ' ⊢ M : B
(dependent evars: ?1169 using ,)
inversion H1; subst; clear H1.5 subgoals, subgoal 1 (ID 1383)
A : Term
Γ : Env
Γ' : Env
H2 : Γ →e Γ'
IHBeta_env : forall (A : Term) (v : nat),
A ↓ v ⊂ Γ -> Γ ⊣ -> Γ' ⊣ -> Γ' ⊢ #v : A
AA : Term
H : A :: Γ ⊣
n : nat
H7 : AA ↓ n ∈ Γ
s : X.Sorts
H3 : Γ' ⊢ A : !s
============================
A :: Γ' ⊢ #n ↑ 1 : AA ↑ (S n) ↑ 1
subgoal 2 (ID 900) is:
Γ' ⊢ Π (A), B : !u
subgoal 3 (ID 903) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 4 (ID 906) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 5 (ID 909) is:
Γ' ⊢ M : B
(dependent evars: ?1169 using ,)
apply thinning with s; trivial. 5 subgoals, subgoal 1 (ID 1384)
A : Term
Γ : Env
Γ' : Env
H2 : Γ →e Γ'
IHBeta_env : forall (A : Term) (v : nat),
A ↓ v ⊂ Γ -> Γ ⊣ -> Γ' ⊣ -> Γ' ⊢ #v : A
AA : Term
H : A :: Γ ⊣
n : nat
H7 : AA ↓ n ∈ Γ
s : X.Sorts
H3 : Γ' ⊢ A : !s
============================
Γ' ⊢ #n : AA ↑ (S n)
subgoal 2 (ID 900) is:
Γ' ⊢ Π (A), B : !u
subgoal 3 (ID 903) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 4 (ID 906) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 5 (ID 909) is:
Γ' ⊢ M : B
(dependent evars: ?1169 using ,)
apply IHBeta_env. 7 subgoals, subgoal 1 (ID 1386)
A : Term
Γ : Env
Γ' : Env
H2 : Γ →e Γ'
IHBeta_env : forall (A : Term) (v : nat),
A ↓ v ⊂ Γ -> Γ ⊣ -> Γ' ⊣ -> Γ' ⊢ #v : A
AA : Term
H : A :: Γ ⊣
n : nat
H7 : AA ↓ n ∈ Γ
s : X.Sorts
H3 : Γ' ⊢ A : !s
============================
AA ↑ (S n) ↓ n ⊂ Γ
subgoal 2 (ID 1387) is:
Γ ⊣
subgoal 3 (ID 1388) is:
Γ' ⊣
subgoal 4 (ID 900) is:
Γ' ⊢ Π (A), B : !u
subgoal 5 (ID 903) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 6 (ID 906) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 7 (ID 909) is:
Γ' ⊢ M : B
(dependent evars: ?1169 using ,)
eauto. 6 subgoals, subgoal 1 (ID 1387)
A : Term
Γ : Env
Γ' : Env
H2 : Γ →e Γ'
IHBeta_env : forall (A : Term) (v : nat),
A ↓ v ⊂ Γ -> Γ ⊣ -> Γ' ⊣ -> Γ' ⊢ #v : A
AA : Term
H : A :: Γ ⊣
n : nat
H7 : AA ↓ n ∈ Γ
s : X.Sorts
H3 : Γ' ⊢ A : !s
============================
Γ ⊣
subgoal 2 (ID 1388) is:
Γ' ⊣
subgoal 3 (ID 900) is:
Γ' ⊢ Π (A), B : !u
subgoal 4 (ID 903) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 5 (ID 906) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 6 (ID 909) is:
Γ' ⊢ M : B
(dependent evars: ?1169 using , ?1390 using ,)
inversion H; subst; clear H. 6 subgoals, subgoal 1 (ID 1443)
A : Term
Γ : Env
Γ' : Env
H2 : Γ →e Γ'
IHBeta_env : forall (A : Term) (v : nat),
A ↓ v ⊂ Γ -> Γ ⊣ -> Γ' ⊣ -> Γ' ⊢ #v : A
AA : Term
n : nat
H7 : AA ↓ n ∈ Γ
s : X.Sorts
H3 : Γ' ⊢ A : !s
s0 : X.Sorts
H1 : Γ ⊢ A : !s0
============================
Γ ⊣
subgoal 2 (ID 1388) is:
Γ' ⊣
subgoal 3 (ID 900) is:
Γ' ⊢ Π (A), B : !u
subgoal 4 (ID 903) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 5 (ID 906) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 6 (ID 909) is:
Γ' ⊢ M : B
(dependent evars: ?1169 using , ?1390 using ,)
eauto.5 subgoals, subgoal 1 (ID 1388)
A : Term
Γ : Env
Γ' : Env
H2 : Γ →e Γ'
IHBeta_env : forall (A : Term) (v : nat),
A ↓ v ⊂ Γ -> Γ ⊣ -> Γ' ⊣ -> Γ' ⊢ #v : A
AA : Term
H : A :: Γ ⊣
n : nat
H7 : AA ↓ n ∈ Γ
s : X.Sorts
H3 : Γ' ⊢ A : !s
============================
Γ' ⊣
subgoal 2 (ID 900) is:
Γ' ⊢ Π (A), B : !u
subgoal 3 (ID 903) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 4 (ID 906) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 5 (ID 909) is:
Γ' ⊢ M : B
(dependent evars: ?1169 using , ?1390 using , ?1444 using , ?1445 using ,)
eauto.4 subgoals, subgoal 1 (ID 900)
Γ : Env
A : Term
B : Term
s : X.Sorts
t : X.Sorts
u : X.Sorts
H : Y.Rel s t u
H0 : Γ ⊢ A : !s
H1 : A :: Γ ⊢ B : !t
IHtyp1 : forall Γ' : Env, Γ' ⊣ -> Γ →e Γ' -> Γ' ⊢ A : !s
IHtyp2 : forall Γ' : Env, Γ' ⊣ -> (A :: Γ) →e Γ' -> Γ' ⊢ B : !t
Γ' : Env
H2 : Γ' ⊣
H3 : Γ →e Γ'
============================
Γ' ⊢ Π (A), B : !u
subgoal 2 (ID 903) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 3 (ID 906) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 4 (ID 909) is:
Γ' ⊢ M : B
(dependent evars: ?1169 using , ?1390 using , ?1444 using , ?1445 using , ?1498 using , ?1499 using ,)
econstructor. 6 subgoals, subgoal 1 (ID 1561)
Γ : Env
A : Term
B : Term
s : X.Sorts
t : X.Sorts
u : X.Sorts
H : Y.Rel s t u
H0 : Γ ⊢ A : !s
H1 : A :: Γ ⊢ B : !t
IHtyp1 : forall Γ' : Env, Γ' ⊣ -> Γ →e Γ' -> Γ' ⊢ A : !s
IHtyp2 : forall Γ' : Env, Γ' ⊣ -> (A :: Γ) →e Γ' -> Γ' ⊢ B : !t
Γ' : Env
H2 : Γ' ⊣
H3 : Γ →e Γ'
============================
Y.Rel ?1559 ?1560 u
subgoal 2 (ID 1562) is:
Γ' ⊢ A : !?1559
subgoal 3 (ID 1563) is:
A :: Γ' ⊢ B : !?1560
subgoal 4 (ID 903) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 5 (ID 906) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 6 (ID 909) is:
Γ' ⊢ M : B
(dependent evars: ?1169 using , ?1390 using , ?1444 using , ?1445 using , ?1498 using , ?1499 using , ?1559 open, ?1560 open,)
apply H. 5 subgoals, subgoal 1 (ID 1562)
Γ : Env
A : Term
B : Term
s : X.Sorts
t : X.Sorts
u : X.Sorts
H : Y.Rel s t u
H0 : Γ ⊢ A : !s
H1 : A :: Γ ⊢ B : !t
IHtyp1 : forall Γ' : Env, Γ' ⊣ -> Γ →e Γ' -> Γ' ⊢ A : !s
IHtyp2 : forall Γ' : Env, Γ' ⊣ -> (A :: Γ) →e Γ' -> Γ' ⊢ B : !t
Γ' : Env
H2 : Γ' ⊣
H3 : Γ →e Γ'
============================
Γ' ⊢ A : !s
subgoal 2 (ID 1563) is:
A :: Γ' ⊢ B : !t
subgoal 3 (ID 903) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 4 (ID 906) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 5 (ID 909) is:
Γ' ⊢ M : B
(dependent evars: ?1169 using , ?1390 using , ?1444 using , ?1445 using , ?1498 using , ?1499 using , ?1559 using , ?1560 using ,)
apply IHtyp1; eauto. 4 subgoals, subgoal 1 (ID 1563)
Γ : Env
A : Term
B : Term
s : X.Sorts
t : X.Sorts
u : X.Sorts
H : Y.Rel s t u
H0 : Γ ⊢ A : !s
H1 : A :: Γ ⊢ B : !t
IHtyp1 : forall Γ' : Env, Γ' ⊣ -> Γ →e Γ' -> Γ' ⊢ A : !s
IHtyp2 : forall Γ' : Env, Γ' ⊣ -> (A :: Γ) →e Γ' -> Γ' ⊢ B : !t
Γ' : Env
H2 : Γ' ⊣
H3 : Γ →e Γ'
============================
A :: Γ' ⊢ B : !t
subgoal 2 (ID 903) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 3 (ID 906) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 4 (ID 909) is:
Γ' ⊢ M : B
(dependent evars: ?1169 using , ?1390 using , ?1444 using , ?1445 using , ?1498 using , ?1499 using , ?1559 using , ?1560 using ,)
apply IHtyp2; eauto.3 subgoals, subgoal 1 (ID 903)
Γ : Env
A : Term
B : Term
M : Term
s1 : X.Sorts
s2 : X.Sorts
s3 : X.Sorts
H : Y.Rel s1 s2 s3
H0 : Γ ⊢ A : !s1
H1 : A :: Γ ⊢ B : !s2
H2 : A :: Γ ⊢ M : B
IHtyp1 : forall Γ' : Env, Γ' ⊣ -> Γ →e Γ' -> Γ' ⊢ A : !s1
IHtyp2 : forall Γ' : Env, Γ' ⊣ -> (A :: Γ) →e Γ' -> Γ' ⊢ B : !s2
IHtyp3 : forall Γ' : Env, Γ' ⊣ -> (A :: Γ) →e Γ' -> Γ' ⊢ M : B
Γ' : Env
H3 : Γ' ⊣
H4 : Γ →e Γ'
============================
Γ' ⊢ λ [A], M : Π (A), B
subgoal 2 (ID 906) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 3 (ID 909) is:
Γ' ⊢ M : B
(dependent evars: ?1169 using , ?1390 using , ?1444 using , ?1445 using , ?1498 using , ?1499 using , ?1559 using , ?1560 using , ?1571 using ,)
econstructor. 6 subgoals, subgoal 1 (ID 1594)
Γ : Env
A : Term
B : Term
M : Term
s1 : X.Sorts
s2 : X.Sorts
s3 : X.Sorts
H : Y.Rel s1 s2 s3
H0 : Γ ⊢ A : !s1
H1 : A :: Γ ⊢ B : !s2
H2 : A :: Γ ⊢ M : B
IHtyp1 : forall Γ' : Env, Γ' ⊣ -> Γ →e Γ' -> Γ' ⊢ A : !s1
IHtyp2 : forall Γ' : Env, Γ' ⊣ -> (A :: Γ) →e Γ' -> Γ' ⊢ B : !s2
IHtyp3 : forall Γ' : Env, Γ' ⊣ -> (A :: Γ) →e Γ' -> Γ' ⊢ M : B
Γ' : Env
H3 : Γ' ⊣
H4 : Γ →e Γ'
============================
Y.Rel ?1591 ?1592 ?1593
subgoal 2 (ID 1595) is:
Γ' ⊢ A : !?1591
subgoal 3 (ID 1596) is:
A :: Γ' ⊢ B : !?1592
subgoal 4 (ID 1597) is:
A :: Γ' ⊢ M : B
subgoal 5 (ID 906) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 6 (ID 909) is:
Γ' ⊢ M : B
(dependent evars: ?1169 using , ?1390 using , ?1444 using , ?1445 using , ?1498 using , ?1499 using , ?1559 using , ?1560 using , ?1571 using , ?1591 open, ?1592 open, ?1593 open,)
apply H. 5 subgoals, subgoal 1 (ID 1595)
Γ : Env
A : Term
B : Term
M : Term
s1 : X.Sorts
s2 : X.Sorts
s3 : X.Sorts
H : Y.Rel s1 s2 s3
H0 : Γ ⊢ A : !s1
H1 : A :: Γ ⊢ B : !s2
H2 : A :: Γ ⊢ M : B
IHtyp1 : forall Γ' : Env, Γ' ⊣ -> Γ →e Γ' -> Γ' ⊢ A : !s1
IHtyp2 : forall Γ' : Env, Γ' ⊣ -> (A :: Γ) →e Γ' -> Γ' ⊢ B : !s2
IHtyp3 : forall Γ' : Env, Γ' ⊣ -> (A :: Γ) →e Γ' -> Γ' ⊢ M : B
Γ' : Env
H3 : Γ' ⊣
H4 : Γ →e Γ'
============================
Γ' ⊢ A : !s1
subgoal 2 (ID 1596) is:
A :: Γ' ⊢ B : !s2
subgoal 3 (ID 1597) is:
A :: Γ' ⊢ M : B
subgoal 4 (ID 906) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 5 (ID 909) is:
Γ' ⊢ M : B
(dependent evars: ?1169 using , ?1390 using , ?1444 using , ?1445 using , ?1498 using , ?1499 using , ?1559 using , ?1560 using , ?1571 using , ?1591 using , ?1592 using , ?1593 using ,)
apply IHtyp1; eauto. 4 subgoals, subgoal 1 (ID 1596)
Γ : Env
A : Term
B : Term
M : Term
s1 : X.Sorts
s2 : X.Sorts
s3 : X.Sorts
H : Y.Rel s1 s2 s3
H0 : Γ ⊢ A : !s1
H1 : A :: Γ ⊢ B : !s2
H2 : A :: Γ ⊢ M : B
IHtyp1 : forall Γ' : Env, Γ' ⊣ -> Γ →e Γ' -> Γ' ⊢ A : !s1
IHtyp2 : forall Γ' : Env, Γ' ⊣ -> (A :: Γ) →e Γ' -> Γ' ⊢ B : !s2
IHtyp3 : forall Γ' : Env, Γ' ⊣ -> (A :: Γ) →e Γ' -> Γ' ⊢ M : B
Γ' : Env
H3 : Γ' ⊣
H4 : Γ →e Γ'
============================
A :: Γ' ⊢ B : !s2
subgoal 2 (ID 1597) is:
A :: Γ' ⊢ M : B
subgoal 3 (ID 906) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 4 (ID 909) is:
Γ' ⊢ M : B
(dependent evars: ?1169 using , ?1390 using , ?1444 using , ?1445 using , ?1498 using , ?1499 using , ?1559 using , ?1560 using , ?1571 using , ?1591 using , ?1592 using , ?1593 using ,)
apply IHtyp2; eauto. 3 subgoals, subgoal 1 (ID 1597)
Γ : Env
A : Term
B : Term
M : Term
s1 : X.Sorts
s2 : X.Sorts
s3 : X.Sorts
H : Y.Rel s1 s2 s3
H0 : Γ ⊢ A : !s1
H1 : A :: Γ ⊢ B : !s2
H2 : A :: Γ ⊢ M : B
IHtyp1 : forall Γ' : Env, Γ' ⊣ -> Γ →e Γ' -> Γ' ⊢ A : !s1
IHtyp2 : forall Γ' : Env, Γ' ⊣ -> (A :: Γ) →e Γ' -> Γ' ⊢ B : !s2
IHtyp3 : forall Γ' : Env, Γ' ⊣ -> (A :: Γ) →e Γ' -> Γ' ⊢ M : B
Γ' : Env
H3 : Γ' ⊣
H4 : Γ →e Γ'
============================
A :: Γ' ⊢ M : B
subgoal 2 (ID 906) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 3 (ID 909) is:
Γ' ⊢ M : B
(dependent evars: ?1169 using , ?1390 using , ?1444 using , ?1445 using , ?1498 using , ?1499 using , ?1559 using , ?1560 using , ?1571 using , ?1591 using , ?1592 using , ?1593 using , ?1605 using ,)
apply IHtyp3; eauto.2 subgoals, subgoal 1 (ID 906)
Γ : Env
M : Term
N : Term
A : Term
B : Term
H : Γ ⊢ M : Π (A), B
H0 : Γ ⊢ N : A
IHtyp1 : forall Γ' : Env, Γ' ⊣ -> Γ →e Γ' -> Γ' ⊢ M : Π (A), B
IHtyp2 : forall Γ' : Env, Γ' ⊣ -> Γ →e Γ' -> Γ' ⊢ N : A
Γ' : Env
H1 : Γ' ⊣
H2 : Γ →e Γ'
============================
Γ' ⊢ M · N : B [ ← N]
subgoal 2 (ID 909) is:
Γ' ⊢ M : B
(dependent evars: ?1169 using , ?1390 using , ?1444 using , ?1445 using , ?1498 using , ?1499 using , ?1559 using , ?1560 using , ?1571 using , ?1591 using , ?1592 using , ?1593 using , ?1605 using , ?1623 using ,)
econstructor. 3 subgoals, subgoal 1 (ID 1645)
Γ : Env
M : Term
N : Term
A : Term
B : Term
H : Γ ⊢ M : Π (A), B
H0 : Γ ⊢ N : A
IHtyp1 : forall Γ' : Env, Γ' ⊣ -> Γ →e Γ' -> Γ' ⊢ M : Π (A), B
IHtyp2 : forall Γ' : Env, Γ' ⊣ -> Γ →e Γ' -> Γ' ⊢ N : A
Γ' : Env
H1 : Γ' ⊣
H2 : Γ →e Γ'
============================
Γ' ⊢ M : Π (?1644), B
subgoal 2 (ID 1646) is:
Γ' ⊢ N : ?1644
subgoal 3 (ID 909) is:
Γ' ⊢ M : B
(dependent evars: ?1169 using , ?1390 using , ?1444 using , ?1445 using , ?1498 using , ?1499 using , ?1559 using , ?1560 using , ?1571 using , ?1591 using , ?1592 using , ?1593 using , ?1605 using , ?1623 using , ?1644 open,)
apply IHtyp1; eauto. 2 subgoals, subgoal 1 (ID 1646)
Γ : Env
M : Term
N : Term
A : Term
B : Term
H : Γ ⊢ M : Π (A), B
H0 : Γ ⊢ N : A
IHtyp1 : forall Γ' : Env, Γ' ⊣ -> Γ →e Γ' -> Γ' ⊢ M : Π (A), B
IHtyp2 : forall Γ' : Env, Γ' ⊣ -> Γ →e Γ' -> Γ' ⊢ N : A
Γ' : Env
H1 : Γ' ⊣
H2 : Γ →e Γ'
============================
Γ' ⊢ N : A
subgoal 2 (ID 909) is:
Γ' ⊢ M : B
(dependent evars: ?1169 using , ?1390 using , ?1444 using , ?1445 using , ?1498 using , ?1499 using , ?1559 using , ?1560 using , ?1571 using , ?1591 using , ?1592 using , ?1593 using , ?1605 using , ?1623 using , ?1644 using ,)
apply IHtyp2; eauto.1 subgoals, subgoal 1 (ID 909)
Γ : Env
M : Term
A : Term
B : Term
s : X.Sorts
H : A ≡ B
H0 : Γ ⊢ M : A
H1 : Γ ⊢ B : !s
IHtyp1 : forall Γ' : Env, Γ' ⊣ -> Γ →e Γ' -> Γ' ⊢ M : A
IHtyp2 : forall Γ' : Env, Γ' ⊣ -> Γ →e Γ' -> Γ' ⊢ B : !s
Γ' : Env
H2 : Γ' ⊣
H3 : Γ →e Γ'
============================
Γ' ⊢ M : B
(dependent evars: ?1169 using , ?1390 using , ?1444 using , ?1445 using , ?1498 using , ?1499 using , ?1559 using , ?1560 using , ?1571 using , ?1591 using , ?1592 using , ?1593 using , ?1605 using , ?1623 using , ?1644 using ,)
econstructor. 3 subgoals, subgoal 1 (ID 1665)
Γ : Env
M : Term
A : Term
B : Term
s : X.Sorts
H : A ≡ B
H0 : Γ ⊢ M : A
H1 : Γ ⊢ B : !s
IHtyp1 : forall Γ' : Env, Γ' ⊣ -> Γ →e Γ' -> Γ' ⊢ M : A
IHtyp2 : forall Γ' : Env, Γ' ⊣ -> Γ →e Γ' -> Γ' ⊢ B : !s
Γ' : Env
H2 : Γ' ⊣
H3 : Γ →e Γ'
============================
?1663 ≡ B
subgoal 2 (ID 1666) is:
Γ' ⊢ M : ?1663
subgoal 3 (ID 1667) is:
Γ' ⊢ B : !?1664
(dependent evars: ?1169 using , ?1390 using , ?1444 using , ?1445 using , ?1498 using , ?1499 using , ?1559 using , ?1560 using , ?1571 using , ?1591 using , ?1592 using , ?1593 using , ?1605 using , ?1623 using , ?1644 using , ?1663 open, ?1664 open,)
apply H. 2 subgoals, subgoal 1 (ID 1666)
Γ : Env
M : Term
A : Term
B : Term
s : X.Sorts
H : A ≡ B
H0 : Γ ⊢ M : A
H1 : Γ ⊢ B : !s
IHtyp1 : forall Γ' : Env, Γ' ⊣ -> Γ →e Γ' -> Γ' ⊢ M : A
IHtyp2 : forall Γ' : Env, Γ' ⊣ -> Γ →e Γ' -> Γ' ⊢ B : !s
Γ' : Env
H2 : Γ' ⊣
H3 : Γ →e Γ'
============================
Γ' ⊢ M : A
subgoal 2 (ID 1667) is:
Γ' ⊢ B : !?1664
(dependent evars: ?1169 using , ?1390 using , ?1444 using , ?1445 using , ?1498 using , ?1499 using , ?1559 using , ?1560 using , ?1571 using , ?1591 using , ?1592 using , ?1593 using , ?1605 using , ?1623 using , ?1644 using , ?1663 using , ?1664 open,)
eapply IHtyp1; eauto. 1 subgoals, subgoal 1 (ID 1667)
Γ : Env
M : Term
A : Term
B : Term
s : X.Sorts
H : A ≡ B
H0 : Γ ⊢ M : A
H1 : Γ ⊢ B : !s
IHtyp1 : forall Γ' : Env, Γ' ⊣ -> Γ →e Γ' -> Γ' ⊢ M : A
IHtyp2 : forall Γ' : Env, Γ' ⊣ -> Γ →e Γ' -> Γ' ⊢ B : !s
Γ' : Env
H2 : Γ' ⊣
H3 : Γ →e Γ'
============================
Γ' ⊢ B : !?1664
(dependent evars: ?1169 using , ?1390 using , ?1444 using , ?1445 using , ?1498 using , ?1499 using , ?1559 using , ?1560 using , ?1571 using , ?1591 using , ?1592 using , ?1593 using , ?1605 using , ?1623 using , ?1644 using , ?1663 using , ?1664 open,)
apply IHtyp2; eauto.No more subgoals.
(dependent evars: ?1169 using , ?1390 using , ?1444 using , ?1445 using , ?1498 using , ?1499 using , ?1559 using , ?1560 using , ?1571 using , ?1591 using , ?1592 using , ?1593 using , ?1605 using , ?1623 using , ?1644 using , ?1663 using , ?1664 using ,)
Qed.Beta_env_sound is defined
Same with expansion in the context.
Lemma Beta_env_sound_up : forall Γ M T, Γ ⊢ M : T -> forall Γ', Γ' ⊣ -> Γ' →e Γ -> Γ' ⊢ M : T .1 subgoals, subgoal 1 (ID 1682)
============================
forall (Γ : Env) (M T : Term),
Γ ⊢ M : T -> forall Γ' : Env, Γ' ⊣ -> Γ' →e Γ -> Γ' ⊢ M : T
(dependent evars:)
induction 1; intros.6 subgoals, subgoal 1 (ID 1778)
Γ : Env
s : X.Sorts
t : X.Sorts
H : Y.Ax s t
H0 : Γ ⊣
Γ' : Env
H1 : Γ' ⊣
H2 : Γ' →e Γ
============================
Γ' ⊢ !s : !t
subgoal 2 (ID 1781) is:
Γ' ⊢ #v : A
subgoal 3 (ID 1784) is:
Γ' ⊢ Π (A), B : !u
subgoal 4 (ID 1787) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 5 (ID 1790) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 6 (ID 1793) is:
Γ' ⊢ M : B
(dependent evars:)
constructor; trivial.5 subgoals, subgoal 1 (ID 1781)
Γ : Env
A : Term
v : nat
H : Γ ⊣
H0 : A ↓ v ⊂ Γ
Γ' : Env
H1 : Γ' ⊣
H2 : Γ' →e Γ
============================
Γ' ⊢ #v : A
subgoal 2 (ID 1784) is:
Γ' ⊢ Π (A), B : !u
subgoal 3 (ID 1787) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 4 (ID 1790) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 5 (ID 1793) is:
Γ' ⊢ M : B
(dependent evars:)
revert A v H0 H H1. 5 subgoals, subgoal 1 (ID 1798)
Γ : Env
Γ' : Env
H2 : Γ' →e Γ
============================
forall (A : Term) (v : nat), A ↓ v ⊂ Γ -> Γ ⊣ -> Γ' ⊣ -> Γ' ⊢ #v : A
subgoal 2 (ID 1784) is:
Γ' ⊢ Π (A), B : !u
subgoal 3 (ID 1787) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 4 (ID 1790) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 5 (ID 1793) is:
Γ' ⊢ M : B
(dependent evars:)
induction H2; intros. 6 subgoals, subgoal 1 (ID 1820)
A : Term
B : Term
Γ : list Term
H : A → B
A0 : Term
v : nat
H0 : A0 ↓ v ⊂ B :: Γ
H1 : B :: Γ ⊣
H2 : A :: Γ ⊣
============================
A :: Γ ⊢ #v : A0
subgoal 2 (ID 1825) is:
A :: Γ ⊢ #v : A0
subgoal 3 (ID 1784) is:
Γ' ⊢ Π (A), B : !u
subgoal 4 (ID 1787) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 5 (ID 1790) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 6 (ID 1793) is:
Γ' ⊢ M : B
(dependent evars:)
destruct H0 as (AA& ? & ?). 6 subgoals, subgoal 1 (ID 1836)
A : Term
B : Term
Γ : list Term
H : A → B
A0 : Term
v : nat
AA : Term
H0 : A0 = AA ↑ (S v)
H3 : AA ↓ v ∈ B :: Γ
H1 : B :: Γ ⊣
H2 : A :: Γ ⊣
============================
A :: Γ ⊢ #v : A0
subgoal 2 (ID 1825) is:
A :: Γ ⊢ #v : A0
subgoal 3 (ID 1784) is:
Γ' ⊢ Π (A), B : !u
subgoal 4 (ID 1787) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 5 (ID 1790) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 6 (ID 1793) is:
Γ' ⊢ M : B
(dependent evars:)
inversion H3; subst; clear H3.7 subgoals, subgoal 1 (ID 1925)
A : Term
B : Term
Γ : list Term
H : A → B
H1 : B :: Γ ⊣
H2 : A :: Γ ⊣
============================
A :: Γ ⊢ #0 : B ↑ 1
subgoal 2 (ID 1926) is:
A :: Γ ⊢ #(S n) : AA ↑ (S (S n))
subgoal 3 (ID 1825) is:
A :: Γ ⊢ #v : A0
subgoal 4 (ID 1784) is:
Γ' ⊢ Π (A), B : !u
subgoal 5 (ID 1787) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 6 (ID 1790) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 7 (ID 1793) is:
Γ' ⊢ M : B
(dependent evars:)
inversion H1; subst; clear H1. 7 subgoals, subgoal 1 (ID 1975)
A : Term
B : Term
Γ : list Term
H : A → B
H2 : A :: Γ ⊣
s : X.Sorts
H3 : Γ ⊢ B : !s
============================
A :: Γ ⊢ #0 : B ↑ 1
subgoal 2 (ID 1926) is:
A :: Γ ⊢ #(S n) : AA ↑ (S (S n))
subgoal 3 (ID 1825) is:
A :: Γ ⊢ #v : A0
subgoal 4 (ID 1784) is:
Γ' ⊢ Π (A), B : !u
subgoal 5 (ID 1787) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 6 (ID 1790) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 7 (ID 1793) is:
Γ' ⊢ M : B
(dependent evars:)
inversion H2; subst; clear H2.7 subgoals, subgoal 1 (ID 2024)
A : Term
B : Term
Γ : list Term
H : A → B
s : X.Sorts
H3 : Γ ⊢ B : !s
s0 : X.Sorts
H1 : Γ ⊢ A : !s0
============================
A :: Γ ⊢ #0 : B ↑ 1
subgoal 2 (ID 1926) is:
A :: Γ ⊢ #(S n) : AA ↑ (S (S n))
subgoal 3 (ID 1825) is:
A :: Γ ⊢ #v : A0
subgoal 4 (ID 1784) is:
Γ' ⊢ Π (A), B : !u
subgoal 5 (ID 1787) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 6 (ID 1790) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 7 (ID 1793) is:
Γ' ⊢ M : B
(dependent evars:)
apply Cnv with ( A ↑ 1 ) s. 9 subgoals, subgoal 1 (ID 2025)
A : Term
B : Term
Γ : list Term
H : A → B
s : X.Sorts
H3 : Γ ⊢ B : !s
s0 : X.Sorts
H1 : Γ ⊢ A : !s0
============================
A ↑ 1 ≡ B ↑ 1
subgoal 2 (ID 2026) is:
A :: Γ ⊢ #0 : A ↑ 1
subgoal 3 (ID 2027) is:
A :: Γ ⊢ B ↑ 1 : !s
subgoal 4 (ID 1926) is:
A :: Γ ⊢ #(S n) : AA ↑ (S (S n))
subgoal 5 (ID 1825) is:
A :: Γ ⊢ #v : A0
subgoal 6 (ID 1784) is:
Γ' ⊢ Π (A), B : !u
subgoal 7 (ID 1787) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 8 (ID 1790) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 9 (ID 1793) is:
Γ' ⊢ M : B
(dependent evars:)
intuition.8 subgoals, subgoal 1 (ID 2026)
A : Term
B : Term
Γ : list Term
H : A → B
s : X.Sorts
H3 : Γ ⊢ B : !s
s0 : X.Sorts
H1 : Γ ⊢ A : !s0
============================
A :: Γ ⊢ #0 : A ↑ 1
subgoal 2 (ID 2027) is:
A :: Γ ⊢ B ↑ 1 : !s
subgoal 3 (ID 1926) is:
A :: Γ ⊢ #(S n) : AA ↑ (S (S n))
subgoal 4 (ID 1825) is:
A :: Γ ⊢ #v : A0
subgoal 5 (ID 1784) is:
Γ' ⊢ Π (A), B : !u
subgoal 6 (ID 1787) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 7 (ID 1790) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 8 (ID 1793) is:
Γ' ⊢ M : B
(dependent evars:)
constructor. 9 subgoals, subgoal 1 (ID 2055)
A : Term
B : Term
Γ : list Term
H : A → B
s : X.Sorts
H3 : Γ ⊢ B : !s
s0 : X.Sorts
H1 : Γ ⊢ A : !s0
============================
A :: Γ ⊣
subgoal 2 (ID 2056) is:
A ↑ 1 ↓ 0 ⊂ A :: Γ
subgoal 3 (ID 2027) is:
A :: Γ ⊢ B ↑ 1 : !s
subgoal 4 (ID 1926) is:
A :: Γ ⊢ #(S n) : AA ↑ (S (S n))
subgoal 5 (ID 1825) is:
A :: Γ ⊢ #v : A0
subgoal 6 (ID 1784) is:
Γ' ⊢ Π (A), B : !u
subgoal 7 (ID 1787) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 8 (ID 1790) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 9 (ID 1793) is:
Γ' ⊢ M : B
(dependent evars:)
econstructor; apply H1. 8 subgoals, subgoal 1 (ID 2056)
A : Term
B : Term
Γ : list Term
H : A → B
s : X.Sorts
H3 : Γ ⊢ B : !s
s0 : X.Sorts
H1 : Γ ⊢ A : !s0
============================
A ↑ 1 ↓ 0 ⊂ A :: Γ
subgoal 2 (ID 2027) is:
A :: Γ ⊢ B ↑ 1 : !s
subgoal 3 (ID 1926) is:
A :: Γ ⊢ #(S n) : AA ↑ (S (S n))
subgoal 4 (ID 1825) is:
A :: Γ ⊢ #v : A0
subgoal 5 (ID 1784) is:
Γ' ⊢ Π (A), B : !u
subgoal 6 (ID 1787) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 7 (ID 1790) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 8 (ID 1793) is:
Γ' ⊢ M : B
(dependent evars: ?2059 using ,)
exists A; intuition.7 subgoals, subgoal 1 (ID 2027)
A : Term
B : Term
Γ : list Term
H : A → B
s : X.Sorts
H3 : Γ ⊢ B : !s
s0 : X.Sorts
H1 : Γ ⊢ A : !s0
============================
A :: Γ ⊢ B ↑ 1 : !s
subgoal 2 (ID 1926) is:
A :: Γ ⊢ #(S n) : AA ↑ (S (S n))
subgoal 3 (ID 1825) is:
A :: Γ ⊢ #v : A0
subgoal 4 (ID 1784) is:
Γ' ⊢ Π (A), B : !u
subgoal 5 (ID 1787) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 6 (ID 1790) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 7 (ID 1793) is:
Γ' ⊢ M : B
(dependent evars: ?2059 using ,)
change !s with !s ↑ 1. 7 subgoals, subgoal 1 (ID 2077)
A : Term
B : Term
Γ : list Term
H : A → B
s : X.Sorts
H3 : Γ ⊢ B : !s
s0 : X.Sorts
H1 : Γ ⊢ A : !s0
============================
A :: Γ ⊢ B ↑ 1 : !s ↑ 1
subgoal 2 (ID 1926) is:
A :: Γ ⊢ #(S n) : AA ↑ (S (S n))
subgoal 3 (ID 1825) is:
A :: Γ ⊢ #v : A0
subgoal 4 (ID 1784) is:
Γ' ⊢ Π (A), B : !u
subgoal 5 (ID 1787) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 6 (ID 1790) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 7 (ID 1793) is:
Γ' ⊢ M : B
(dependent evars: ?2059 using ,)
apply thinning with s0 ;trivial.6 subgoals, subgoal 1 (ID 1926)
A : Term
B : Term
Γ : list Term
H : A → B
AA : Term
H1 : B :: Γ ⊣
H2 : A :: Γ ⊣
n : nat
H7 : AA ↓ n ∈ Γ
============================
A :: Γ ⊢ #(S n) : AA ↑ (S (S n))
subgoal 2 (ID 1825) is:
A :: Γ ⊢ #v : A0
subgoal 3 (ID 1784) is:
Γ' ⊢ Π (A), B : !u
subgoal 4 (ID 1787) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 5 (ID 1790) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 6 (ID 1793) is:
Γ' ⊢ M : B
(dependent evars: ?2059 using ,)
constructor. 7 subgoals, subgoal 1 (ID 2082)
A : Term
B : Term
Γ : list Term
H : A → B
AA : Term
H1 : B :: Γ ⊣
H2 : A :: Γ ⊣
n : nat
H7 : AA ↓ n ∈ Γ
============================
A :: Γ ⊣
subgoal 2 (ID 2083) is:
AA ↑ (S (S n)) ↓ S n ⊂ A :: Γ
subgoal 3 (ID 1825) is:
A :: Γ ⊢ #v : A0
subgoal 4 (ID 1784) is:
Γ' ⊢ Π (A), B : !u
subgoal 5 (ID 1787) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 6 (ID 1790) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 7 (ID 1793) is:
Γ' ⊢ M : B
(dependent evars: ?2059 using ,)
trivial. 6 subgoals, subgoal 1 (ID 2083)
A : Term
B : Term
Γ : list Term
H : A → B
AA : Term
H1 : B :: Γ ⊣
H2 : A :: Γ ⊣
n : nat
H7 : AA ↓ n ∈ Γ
============================
AA ↑ (S (S n)) ↓ S n ⊂ A :: Γ
subgoal 2 (ID 1825) is:
A :: Γ ⊢ #v : A0
subgoal 3 (ID 1784) is:
Γ' ⊢ Π (A), B : !u
subgoal 4 (ID 1787) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 5 (ID 1790) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 6 (ID 1793) is:
Γ' ⊢ M : B
(dependent evars: ?2059 using ,)
exists AA; intuition.5 subgoals, subgoal 1 (ID 1825)
A : Term
Γ : Env
Γ' : Env
H2 : Γ →e Γ'
IHBeta_env : forall (A : Term) (v : nat),
A ↓ v ⊂ Γ' -> Γ' ⊣ -> Γ ⊣ -> Γ ⊢ #v : A
A0 : Term
v : nat
H0 : A0 ↓ v ⊂ A :: Γ'
H : A :: Γ' ⊣
H1 : A :: Γ ⊣
============================
A :: Γ ⊢ #v : A0
subgoal 2 (ID 1784) is:
Γ' ⊢ Π (A), B : !u
subgoal 3 (ID 1787) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 4 (ID 1790) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 5 (ID 1793) is:
Γ' ⊢ M : B
(dependent evars: ?2059 using ,)
destruct H0 as (AA& ? & ?). 5 subgoals, subgoal 1 (ID 2111)
A : Term
Γ : Env
Γ' : Env
H2 : Γ →e Γ'
IHBeta_env : forall (A : Term) (v : nat),
A ↓ v ⊂ Γ' -> Γ' ⊣ -> Γ ⊣ -> Γ ⊢ #v : A
A0 : Term
v : nat
AA : Term
H0 : A0 = AA ↑ (S v)
H3 : AA ↓ v ∈ A :: Γ'
H : A :: Γ' ⊣
H1 : A :: Γ ⊣
============================
A :: Γ ⊢ #v : A0
subgoal 2 (ID 1784) is:
Γ' ⊢ Π (A), B : !u
subgoal 3 (ID 1787) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 4 (ID 1790) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 5 (ID 1793) is:
Γ' ⊢ M : B
(dependent evars: ?2059 using ,)
inversion H3; subst; clear H3.6 subgoals, subgoal 1 (ID 2200)
A : Term
Γ : Env
Γ' : Env
H2 : Γ →e Γ'
IHBeta_env : forall (A : Term) (v : nat),
A ↓ v ⊂ Γ' -> Γ' ⊣ -> Γ ⊣ -> Γ ⊢ #v : A
H : A :: Γ' ⊣
H1 : A :: Γ ⊣
============================
A :: Γ ⊢ #0 : A ↑ 1
subgoal 2 (ID 2201) is:
A :: Γ ⊢ #(S n) : AA ↑ (S (S n))
subgoal 3 (ID 1784) is:
Γ' ⊢ Π (A), B : !u
subgoal 4 (ID 1787) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 5 (ID 1790) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 6 (ID 1793) is:
Γ' ⊢ M : B
(dependent evars: ?2059 using ,)
constructor. 7 subgoals, subgoal 1 (ID 2204)
A : Term
Γ : Env
Γ' : Env
H2 : Γ →e Γ'
IHBeta_env : forall (A : Term) (v : nat),
A ↓ v ⊂ Γ' -> Γ' ⊣ -> Γ ⊣ -> Γ ⊢ #v : A
H : A :: Γ' ⊣
H1 : A :: Γ ⊣
============================
A :: Γ ⊣
subgoal 2 (ID 2205) is:
A ↑ 1 ↓ 0 ⊂ A :: Γ
subgoal 3 (ID 2201) is:
A :: Γ ⊢ #(S n) : AA ↑ (S (S n))
subgoal 4 (ID 1784) is:
Γ' ⊢ Π (A), B : !u
subgoal 5 (ID 1787) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 6 (ID 1790) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 7 (ID 1793) is:
Γ' ⊢ M : B
(dependent evars: ?2059 using ,)
trivial. 6 subgoals, subgoal 1 (ID 2205)
A : Term
Γ : Env
Γ' : Env
H2 : Γ →e Γ'
IHBeta_env : forall (A : Term) (v : nat),
A ↓ v ⊂ Γ' -> Γ' ⊣ -> Γ ⊣ -> Γ ⊢ #v : A
H : A :: Γ' ⊣
H1 : A :: Γ ⊣
============================
A ↑ 1 ↓ 0 ⊂ A :: Γ
subgoal 2 (ID 2201) is:
A :: Γ ⊢ #(S n) : AA ↑ (S (S n))
subgoal 3 (ID 1784) is:
Γ' ⊢ Π (A), B : !u
subgoal 4 (ID 1787) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 5 (ID 1790) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 6 (ID 1793) is:
Γ' ⊢ M : B
(dependent evars: ?2059 using ,)
exists A; intuition.5 subgoals, subgoal 1 (ID 2201)
A : Term
Γ : Env
Γ' : Env
H2 : Γ →e Γ'
IHBeta_env : forall (A : Term) (v : nat),
A ↓ v ⊂ Γ' -> Γ' ⊣ -> Γ ⊣ -> Γ ⊢ #v : A
AA : Term
H : A :: Γ' ⊣
H1 : A :: Γ ⊣
n : nat
H7 : AA ↓ n ∈ Γ'
============================
A :: Γ ⊢ #(S n) : AA ↑ (S (S n))
subgoal 2 (ID 1784) is:
Γ' ⊢ Π (A), B : !u
subgoal 3 (ID 1787) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 4 (ID 1790) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 5 (ID 1793) is:
Γ' ⊢ M : B
(dependent evars: ?2059 using ,)
change (S(S n)) with (1+S n). 5 subgoals, subgoal 1 (ID 2221)
A : Term
Γ : Env
Γ' : Env
H2 : Γ →e Γ'
IHBeta_env : forall (A : Term) (v : nat),
A ↓ v ⊂ Γ' -> Γ' ⊣ -> Γ ⊣ -> Γ ⊢ #v : A
AA : Term
H : A :: Γ' ⊣
H1 : A :: Γ ⊣
n : nat
H7 : AA ↓ n ∈ Γ'
============================
A :: Γ ⊢ #(S n) : AA ↑ (1 + S n)
subgoal 2 (ID 1784) is:
Γ' ⊢ Π (A), B : !u
subgoal 3 (ID 1787) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 4 (ID 1790) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 5 (ID 1793) is:
Γ' ⊢ M : B
(dependent evars: ?2059 using ,)
change #(S n) with (#n ↑ 1).5 subgoals, subgoal 1 (ID 2223)
A : Term
Γ : Env
Γ' : Env
H2 : Γ →e Γ'
IHBeta_env : forall (A : Term) (v : nat),
A ↓ v ⊂ Γ' -> Γ' ⊣ -> Γ ⊣ -> Γ ⊢ #v : A
AA : Term
H : A :: Γ' ⊣
H1 : A :: Γ ⊣
n : nat
H7 : AA ↓ n ∈ Γ'
============================
A :: Γ ⊢ #n ↑ 1 : AA ↑ (1 + S n)
subgoal 2 (ID 1784) is:
Γ' ⊢ Π (A), B : !u
subgoal 3 (ID 1787) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 4 (ID 1790) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 5 (ID 1793) is:
Γ' ⊢ M : B
(dependent evars: ?2059 using ,)
rewrite <- lift_lift.5 subgoals, subgoal 1 (ID 2224)
A : Term
Γ : Env
Γ' : Env
H2 : Γ →e Γ'
IHBeta_env : forall (A : Term) (v : nat),
A ↓ v ⊂ Γ' -> Γ' ⊣ -> Γ ⊣ -> Γ ⊢ #v : A
AA : Term
H : A :: Γ' ⊣
H1 : A :: Γ ⊣
n : nat
H7 : AA ↓ n ∈ Γ'
============================
A :: Γ ⊢ #n ↑ 1 : AA ↑ (S n) ↑ 1
subgoal 2 (ID 1784) is:
Γ' ⊢ Π (A), B : !u
subgoal 3 (ID 1787) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 4 (ID 1790) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 5 (ID 1793) is:
Γ' ⊢ M : B
(dependent evars: ?2059 using ,)
inversion H1; subst; clear H1.5 subgoals, subgoal 1 (ID 2273)
A : Term
Γ : Env
Γ' : Env
H2 : Γ →e Γ'
IHBeta_env : forall (A : Term) (v : nat),
A ↓ v ⊂ Γ' -> Γ' ⊣ -> Γ ⊣ -> Γ ⊢ #v : A
AA : Term
H : A :: Γ' ⊣
n : nat
H7 : AA ↓ n ∈ Γ'
s : X.Sorts
H3 : Γ ⊢ A : !s
============================
A :: Γ ⊢ #n ↑ 1 : AA ↑ (S n) ↑ 1
subgoal 2 (ID 1784) is:
Γ' ⊢ Π (A), B : !u
subgoal 3 (ID 1787) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 4 (ID 1790) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 5 (ID 1793) is:
Γ' ⊢ M : B
(dependent evars: ?2059 using ,)
apply thinning with s; trivial. 5 subgoals, subgoal 1 (ID 2274)
A : Term
Γ : Env
Γ' : Env
H2 : Γ →e Γ'
IHBeta_env : forall (A : Term) (v : nat),
A ↓ v ⊂ Γ' -> Γ' ⊣ -> Γ ⊣ -> Γ ⊢ #v : A
AA : Term
H : A :: Γ' ⊣
n : nat
H7 : AA ↓ n ∈ Γ'
s : X.Sorts
H3 : Γ ⊢ A : !s
============================
Γ ⊢ #n : AA ↑ (S n)
subgoal 2 (ID 1784) is:
Γ' ⊢ Π (A), B : !u
subgoal 3 (ID 1787) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 4 (ID 1790) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 5 (ID 1793) is:
Γ' ⊢ M : B
(dependent evars: ?2059 using ,)
apply IHBeta_env. 7 subgoals, subgoal 1 (ID 2276)
A : Term
Γ : Env
Γ' : Env
H2 : Γ →e Γ'
IHBeta_env : forall (A : Term) (v : nat),
A ↓ v ⊂ Γ' -> Γ' ⊣ -> Γ ⊣ -> Γ ⊢ #v : A
AA : Term
H : A :: Γ' ⊣
n : nat
H7 : AA ↓ n ∈ Γ'
s : X.Sorts
H3 : Γ ⊢ A : !s
============================
AA ↑ (S n) ↓ n ⊂ Γ'
subgoal 2 (ID 2277) is:
Γ' ⊣
subgoal 3 (ID 2278) is:
Γ ⊣
subgoal 4 (ID 1784) is:
Γ' ⊢ Π (A), B : !u
subgoal 5 (ID 1787) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 6 (ID 1790) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 7 (ID 1793) is:
Γ' ⊢ M : B
(dependent evars: ?2059 using ,)
exists AA; intuition. 6 subgoals, subgoal 1 (ID 2277)
A : Term
Γ : Env
Γ' : Env
H2 : Γ →e Γ'
IHBeta_env : forall (A : Term) (v : nat),
A ↓ v ⊂ Γ' -> Γ' ⊣ -> Γ ⊣ -> Γ ⊢ #v : A
AA : Term
H : A :: Γ' ⊣
n : nat
H7 : AA ↓ n ∈ Γ'
s : X.Sorts
H3 : Γ ⊢ A : !s
============================
Γ' ⊣
subgoal 2 (ID 2278) is:
Γ ⊣
subgoal 3 (ID 1784) is:
Γ' ⊢ Π (A), B : !u
subgoal 4 (ID 1787) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 5 (ID 1790) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 6 (ID 1793) is:
Γ' ⊢ M : B
(dependent evars: ?2059 using ,)
inversion H; subst; clear H. 6 subgoals, subgoal 1 (ID 2333)
A : Term
Γ : Env
Γ' : Env
H2 : Γ →e Γ'
IHBeta_env : forall (A : Term) (v : nat),
A ↓ v ⊂ Γ' -> Γ' ⊣ -> Γ ⊣ -> Γ ⊢ #v : A
AA : Term
n : nat
H7 : AA ↓ n ∈ Γ'
s : X.Sorts
H3 : Γ ⊢ A : !s
s0 : X.Sorts
H1 : Γ' ⊢ A : !s0
============================
Γ' ⊣
subgoal 2 (ID 2278) is:
Γ ⊣
subgoal 3 (ID 1784) is:
Γ' ⊢ Π (A), B : !u
subgoal 4 (ID 1787) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 5 (ID 1790) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 6 (ID 1793) is:
Γ' ⊢ M : B
(dependent evars: ?2059 using ,)
eauto.5 subgoals, subgoal 1 (ID 2278)
A : Term
Γ : Env
Γ' : Env
H2 : Γ →e Γ'
IHBeta_env : forall (A : Term) (v : nat),
A ↓ v ⊂ Γ' -> Γ' ⊣ -> Γ ⊣ -> Γ ⊢ #v : A
AA : Term
H : A :: Γ' ⊣
n : nat
H7 : AA ↓ n ∈ Γ'
s : X.Sorts
H3 : Γ ⊢ A : !s
============================
Γ ⊣
subgoal 2 (ID 1784) is:
Γ' ⊢ Π (A), B : !u
subgoal 3 (ID 1787) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 4 (ID 1790) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 5 (ID 1793) is:
Γ' ⊢ M : B
(dependent evars: ?2059 using , ?2334 using , ?2335 using ,)
eauto.4 subgoals, subgoal 1 (ID 1784)
Γ : Env
A : Term
B : Term
s : X.Sorts
t : X.Sorts
u : X.Sorts
H : Y.Rel s t u
H0 : Γ ⊢ A : !s
H1 : A :: Γ ⊢ B : !t
IHtyp1 : forall Γ' : Env, Γ' ⊣ -> Γ' →e Γ -> Γ' ⊢ A : !s
IHtyp2 : forall Γ' : Env, Γ' ⊣ -> Γ' →e (A :: Γ) -> Γ' ⊢ B : !t
Γ' : Env
H2 : Γ' ⊣
H3 : Γ' →e Γ
============================
Γ' ⊢ Π (A), B : !u
subgoal 2 (ID 1787) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 3 (ID 1790) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 4 (ID 1793) is:
Γ' ⊢ M : B
(dependent evars: ?2059 using , ?2334 using , ?2335 using , ?2388 using , ?2389 using ,)
econstructor. 6 subgoals, subgoal 1 (ID 2451)
Γ : Env
A : Term
B : Term
s : X.Sorts
t : X.Sorts
u : X.Sorts
H : Y.Rel s t u
H0 : Γ ⊢ A : !s
H1 : A :: Γ ⊢ B : !t
IHtyp1 : forall Γ' : Env, Γ' ⊣ -> Γ' →e Γ -> Γ' ⊢ A : !s
IHtyp2 : forall Γ' : Env, Γ' ⊣ -> Γ' →e (A :: Γ) -> Γ' ⊢ B : !t
Γ' : Env
H2 : Γ' ⊣
H3 : Γ' →e Γ
============================
Y.Rel ?2449 ?2450 u
subgoal 2 (ID 2452) is:
Γ' ⊢ A : !?2449
subgoal 3 (ID 2453) is:
A :: Γ' ⊢ B : !?2450
subgoal 4 (ID 1787) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 5 (ID 1790) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 6 (ID 1793) is:
Γ' ⊢ M : B
(dependent evars: ?2059 using , ?2334 using , ?2335 using , ?2388 using , ?2389 using , ?2449 open, ?2450 open,)
apply H. 5 subgoals, subgoal 1 (ID 2452)
Γ : Env
A : Term
B : Term
s : X.Sorts
t : X.Sorts
u : X.Sorts
H : Y.Rel s t u
H0 : Γ ⊢ A : !s
H1 : A :: Γ ⊢ B : !t
IHtyp1 : forall Γ' : Env, Γ' ⊣ -> Γ' →e Γ -> Γ' ⊢ A : !s
IHtyp2 : forall Γ' : Env, Γ' ⊣ -> Γ' →e (A :: Γ) -> Γ' ⊢ B : !t
Γ' : Env
H2 : Γ' ⊣
H3 : Γ' →e Γ
============================
Γ' ⊢ A : !s
subgoal 2 (ID 2453) is:
A :: Γ' ⊢ B : !t
subgoal 3 (ID 1787) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 4 (ID 1790) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 5 (ID 1793) is:
Γ' ⊢ M : B
(dependent evars: ?2059 using , ?2334 using , ?2335 using , ?2388 using , ?2389 using , ?2449 using , ?2450 using ,)
apply IHtyp1; eauto. 4 subgoals, subgoal 1 (ID 2453)
Γ : Env
A : Term
B : Term
s : X.Sorts
t : X.Sorts
u : X.Sorts
H : Y.Rel s t u
H0 : Γ ⊢ A : !s
H1 : A :: Γ ⊢ B : !t
IHtyp1 : forall Γ' : Env, Γ' ⊣ -> Γ' →e Γ -> Γ' ⊢ A : !s
IHtyp2 : forall Γ' : Env, Γ' ⊣ -> Γ' →e (A :: Γ) -> Γ' ⊢ B : !t
Γ' : Env
H2 : Γ' ⊣
H3 : Γ' →e Γ
============================
A :: Γ' ⊢ B : !t
subgoal 2 (ID 1787) is:
Γ' ⊢ λ [A], M : Π (A), B
subgoal 3 (ID 1790) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 4 (ID 1793) is:
Γ' ⊢ M : B
(dependent evars: ?2059 using , ?2334 using , ?2335 using , ?2388 using , ?2389 using , ?2449 using , ?2450 using ,)
apply IHtyp2; eauto.3 subgoals, subgoal 1 (ID 1787)
Γ : Env
A : Term
B : Term
M : Term
s1 : X.Sorts
s2 : X.Sorts
s3 : X.Sorts
H : Y.Rel s1 s2 s3
H0 : Γ ⊢ A : !s1
H1 : A :: Γ ⊢ B : !s2
H2 : A :: Γ ⊢ M : B
IHtyp1 : forall Γ' : Env, Γ' ⊣ -> Γ' →e Γ -> Γ' ⊢ A : !s1
IHtyp2 : forall Γ' : Env, Γ' ⊣ -> Γ' →e (A :: Γ) -> Γ' ⊢ B : !s2
IHtyp3 : forall Γ' : Env, Γ' ⊣ -> Γ' →e (A :: Γ) -> Γ' ⊢ M : B
Γ' : Env
H3 : Γ' ⊣
H4 : Γ' →e Γ
============================
Γ' ⊢ λ [A], M : Π (A), B
subgoal 2 (ID 1790) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 3 (ID 1793) is:
Γ' ⊢ M : B
(dependent evars: ?2059 using , ?2334 using , ?2335 using , ?2388 using , ?2389 using , ?2449 using , ?2450 using , ?2461 using ,)
econstructor. 6 subgoals, subgoal 1 (ID 2484)
Γ : Env
A : Term
B : Term
M : Term
s1 : X.Sorts
s2 : X.Sorts
s3 : X.Sorts
H : Y.Rel s1 s2 s3
H0 : Γ ⊢ A : !s1
H1 : A :: Γ ⊢ B : !s2
H2 : A :: Γ ⊢ M : B
IHtyp1 : forall Γ' : Env, Γ' ⊣ -> Γ' →e Γ -> Γ' ⊢ A : !s1
IHtyp2 : forall Γ' : Env, Γ' ⊣ -> Γ' →e (A :: Γ) -> Γ' ⊢ B : !s2
IHtyp3 : forall Γ' : Env, Γ' ⊣ -> Γ' →e (A :: Γ) -> Γ' ⊢ M : B
Γ' : Env
H3 : Γ' ⊣
H4 : Γ' →e Γ
============================
Y.Rel ?2481 ?2482 ?2483
subgoal 2 (ID 2485) is:
Γ' ⊢ A : !?2481
subgoal 3 (ID 2486) is:
A :: Γ' ⊢ B : !?2482
subgoal 4 (ID 2487) is:
A :: Γ' ⊢ M : B
subgoal 5 (ID 1790) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 6 (ID 1793) is:
Γ' ⊢ M : B
(dependent evars: ?2059 using , ?2334 using , ?2335 using , ?2388 using , ?2389 using , ?2449 using , ?2450 using , ?2461 using , ?2481 open, ?2482 open, ?2483 open,)
apply H. 5 subgoals, subgoal 1 (ID 2485)
Γ : Env
A : Term
B : Term
M : Term
s1 : X.Sorts
s2 : X.Sorts
s3 : X.Sorts
H : Y.Rel s1 s2 s3
H0 : Γ ⊢ A : !s1
H1 : A :: Γ ⊢ B : !s2
H2 : A :: Γ ⊢ M : B
IHtyp1 : forall Γ' : Env, Γ' ⊣ -> Γ' →e Γ -> Γ' ⊢ A : !s1
IHtyp2 : forall Γ' : Env, Γ' ⊣ -> Γ' →e (A :: Γ) -> Γ' ⊢ B : !s2
IHtyp3 : forall Γ' : Env, Γ' ⊣ -> Γ' →e (A :: Γ) -> Γ' ⊢ M : B
Γ' : Env
H3 : Γ' ⊣
H4 : Γ' →e Γ
============================
Γ' ⊢ A : !s1
subgoal 2 (ID 2486) is:
A :: Γ' ⊢ B : !s2
subgoal 3 (ID 2487) is:
A :: Γ' ⊢ M : B
subgoal 4 (ID 1790) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 5 (ID 1793) is:
Γ' ⊢ M : B
(dependent evars: ?2059 using , ?2334 using , ?2335 using , ?2388 using , ?2389 using , ?2449 using , ?2450 using , ?2461 using , ?2481 using , ?2482 using , ?2483 using ,)
apply IHtyp1; eauto. 4 subgoals, subgoal 1 (ID 2486)
Γ : Env
A : Term
B : Term
M : Term
s1 : X.Sorts
s2 : X.Sorts
s3 : X.Sorts
H : Y.Rel s1 s2 s3
H0 : Γ ⊢ A : !s1
H1 : A :: Γ ⊢ B : !s2
H2 : A :: Γ ⊢ M : B
IHtyp1 : forall Γ' : Env, Γ' ⊣ -> Γ' →e Γ -> Γ' ⊢ A : !s1
IHtyp2 : forall Γ' : Env, Γ' ⊣ -> Γ' →e (A :: Γ) -> Γ' ⊢ B : !s2
IHtyp3 : forall Γ' : Env, Γ' ⊣ -> Γ' →e (A :: Γ) -> Γ' ⊢ M : B
Γ' : Env
H3 : Γ' ⊣
H4 : Γ' →e Γ
============================
A :: Γ' ⊢ B : !s2
subgoal 2 (ID 2487) is:
A :: Γ' ⊢ M : B
subgoal 3 (ID 1790) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 4 (ID 1793) is:
Γ' ⊢ M : B
(dependent evars: ?2059 using , ?2334 using , ?2335 using , ?2388 using , ?2389 using , ?2449 using , ?2450 using , ?2461 using , ?2481 using , ?2482 using , ?2483 using ,)
apply IHtyp2; eauto. 3 subgoals, subgoal 1 (ID 2487)
Γ : Env
A : Term
B : Term
M : Term
s1 : X.Sorts
s2 : X.Sorts
s3 : X.Sorts
H : Y.Rel s1 s2 s3
H0 : Γ ⊢ A : !s1
H1 : A :: Γ ⊢ B : !s2
H2 : A :: Γ ⊢ M : B
IHtyp1 : forall Γ' : Env, Γ' ⊣ -> Γ' →e Γ -> Γ' ⊢ A : !s1
IHtyp2 : forall Γ' : Env, Γ' ⊣ -> Γ' →e (A :: Γ) -> Γ' ⊢ B : !s2
IHtyp3 : forall Γ' : Env, Γ' ⊣ -> Γ' →e (A :: Γ) -> Γ' ⊢ M : B
Γ' : Env
H3 : Γ' ⊣
H4 : Γ' →e Γ
============================
A :: Γ' ⊢ M : B
subgoal 2 (ID 1790) is:
Γ' ⊢ M · N : B [ ← N]
subgoal 3 (ID 1793) is:
Γ' ⊢ M : B
(dependent evars: ?2059 using , ?2334 using , ?2335 using , ?2388 using , ?2389 using , ?2449 using , ?2450 using , ?2461 using , ?2481 using , ?2482 using , ?2483 using , ?2495 using ,)
apply IHtyp3; eauto.2 subgoals, subgoal 1 (ID 1790)
Γ : Env
M : Term
N : Term
A : Term
B : Term
H : Γ ⊢ M : Π (A), B
H0 : Γ ⊢ N : A
IHtyp1 : forall Γ' : Env, Γ' ⊣ -> Γ' →e Γ -> Γ' ⊢ M : Π (A), B
IHtyp2 : forall Γ' : Env, Γ' ⊣ -> Γ' →e Γ -> Γ' ⊢ N : A
Γ' : Env
H1 : Γ' ⊣
H2 : Γ' →e Γ
============================
Γ' ⊢ M · N : B [ ← N]
subgoal 2 (ID 1793) is:
Γ' ⊢ M : B
(dependent evars: ?2059 using , ?2334 using , ?2335 using , ?2388 using , ?2389 using , ?2449 using , ?2450 using , ?2461 using , ?2481 using , ?2482 using , ?2483 using , ?2495 using , ?2513 using ,)
econstructor. 3 subgoals, subgoal 1 (ID 2535)
Γ : Env
M : Term
N : Term
A : Term
B : Term
H : Γ ⊢ M : Π (A), B
H0 : Γ ⊢ N : A
IHtyp1 : forall Γ' : Env, Γ' ⊣ -> Γ' →e Γ -> Γ' ⊢ M : Π (A), B
IHtyp2 : forall Γ' : Env, Γ' ⊣ -> Γ' →e Γ -> Γ' ⊢ N : A
Γ' : Env
H1 : Γ' ⊣
H2 : Γ' →e Γ
============================
Γ' ⊢ M : Π (?2534), B
subgoal 2 (ID 2536) is:
Γ' ⊢ N : ?2534
subgoal 3 (ID 1793) is:
Γ' ⊢ M : B
(dependent evars: ?2059 using , ?2334 using , ?2335 using , ?2388 using , ?2389 using , ?2449 using , ?2450 using , ?2461 using , ?2481 using , ?2482 using , ?2483 using , ?2495 using , ?2513 using , ?2534 open,)
apply IHtyp1; eauto. 2 subgoals, subgoal 1 (ID 2536)
Γ : Env
M : Term
N : Term
A : Term
B : Term
H : Γ ⊢ M : Π (A), B
H0 : Γ ⊢ N : A
IHtyp1 : forall Γ' : Env, Γ' ⊣ -> Γ' →e Γ -> Γ' ⊢ M : Π (A), B
IHtyp2 : forall Γ' : Env, Γ' ⊣ -> Γ' →e Γ -> Γ' ⊢ N : A
Γ' : Env
H1 : Γ' ⊣
H2 : Γ' →e Γ
============================
Γ' ⊢ N : A
subgoal 2 (ID 1793) is:
Γ' ⊢ M : B
(dependent evars: ?2059 using , ?2334 using , ?2335 using , ?2388 using , ?2389 using , ?2449 using , ?2450 using , ?2461 using , ?2481 using , ?2482 using , ?2483 using , ?2495 using , ?2513 using , ?2534 using ,)
apply IHtyp2; eauto.1 subgoals, subgoal 1 (ID 1793)
Γ : Env
M : Term
A : Term
B : Term
s : X.Sorts
H : A ≡ B
H0 : Γ ⊢ M : A
H1 : Γ ⊢ B : !s
IHtyp1 : forall Γ' : Env, Γ' ⊣ -> Γ' →e Γ -> Γ' ⊢ M : A
IHtyp2 : forall Γ' : Env, Γ' ⊣ -> Γ' →e Γ -> Γ' ⊢ B : !s
Γ' : Env
H2 : Γ' ⊣
H3 : Γ' →e Γ
============================
Γ' ⊢ M : B
(dependent evars: ?2059 using , ?2334 using , ?2335 using , ?2388 using , ?2389 using , ?2449 using , ?2450 using , ?2461 using , ?2481 using , ?2482 using , ?2483 using , ?2495 using , ?2513 using , ?2534 using ,)
econstructor. 3 subgoals, subgoal 1 (ID 2555)
Γ : Env
M : Term
A : Term
B : Term
s : X.Sorts
H : A ≡ B
H0 : Γ ⊢ M : A
H1 : Γ ⊢ B : !s
IHtyp1 : forall Γ' : Env, Γ' ⊣ -> Γ' →e Γ -> Γ' ⊢ M : A
IHtyp2 : forall Γ' : Env, Γ' ⊣ -> Γ' →e Γ -> Γ' ⊢ B : !s
Γ' : Env
H2 : Γ' ⊣
H3 : Γ' →e Γ
============================
?2553 ≡ B
subgoal 2 (ID 2556) is:
Γ' ⊢ M : ?2553
subgoal 3 (ID 2557) is:
Γ' ⊢ B : !?2554
(dependent evars: ?2059 using , ?2334 using , ?2335 using , ?2388 using , ?2389 using , ?2449 using , ?2450 using , ?2461 using , ?2481 using , ?2482 using , ?2483 using , ?2495 using , ?2513 using , ?2534 using , ?2553 open, ?2554 open,)
apply H. 2 subgoals, subgoal 1 (ID 2556)
Γ : Env
M : Term
A : Term
B : Term
s : X.Sorts
H : A ≡ B
H0 : Γ ⊢ M : A
H1 : Γ ⊢ B : !s
IHtyp1 : forall Γ' : Env, Γ' ⊣ -> Γ' →e Γ -> Γ' ⊢ M : A
IHtyp2 : forall Γ' : Env, Γ' ⊣ -> Γ' →e Γ -> Γ' ⊢ B : !s
Γ' : Env
H2 : Γ' ⊣
H3 : Γ' →e Γ
============================
Γ' ⊢ M : A
subgoal 2 (ID 2557) is:
Γ' ⊢ B : !?2554
(dependent evars: ?2059 using , ?2334 using , ?2335 using , ?2388 using , ?2389 using , ?2449 using , ?2450 using , ?2461 using , ?2481 using , ?2482 using , ?2483 using , ?2495 using , ?2513 using , ?2534 using , ?2553 using , ?2554 open,)
eapply IHtyp1; eauto. 1 subgoals, subgoal 1 (ID 2557)
Γ : Env
M : Term
A : Term
B : Term
s : X.Sorts
H : A ≡ B
H0 : Γ ⊢ M : A
H1 : Γ ⊢ B : !s
IHtyp1 : forall Γ' : Env, Γ' ⊣ -> Γ' →e Γ -> Γ' ⊢ M : A
IHtyp2 : forall Γ' : Env, Γ' ⊣ -> Γ' →e Γ -> Γ' ⊢ B : !s
Γ' : Env
H2 : Γ' ⊣
H3 : Γ' →e Γ
============================
Γ' ⊢ B : !?2554
(dependent evars: ?2059 using , ?2334 using , ?2335 using , ?2388 using , ?2389 using , ?2449 using , ?2450 using , ?2461 using , ?2481 using , ?2482 using , ?2483 using , ?2495 using , ?2513 using , ?2534 using , ?2553 using , ?2554 open,)
apply IHtyp2; eauto.No more subgoals.
(dependent evars: ?2059 using , ?2334 using , ?2335 using , ?2388 using , ?2389 using , ?2449 using , ?2450 using , ?2461 using , ?2481 using , ?2482 using , ?2483 using , ?2495 using , ?2513 using , ?2534 using , ?2553 using , ?2554 using ,)
Qed.Beta_env_sound_up is defined
Second Step: reduction in the term.
Lemma Beta_sound : forall Γ M T, Γ ⊢ M : T -> forall N, M → N -> Γ ⊢ N : T.1 subgoals, subgoal 1 (ID 2572)
============================
forall (Γ : Env) (M T : Term),
Γ ⊢ M : T -> forall N : Term, M → N -> Γ ⊢ N : T
(dependent evars:)
induction 1; intros.6 subgoals, subgoal 1 (ID 2667)
Γ : Env
s : X.Sorts
t : X.Sorts
H : Y.Ax s t
H0 : Γ ⊣
N : Term
H1 : !s → N
============================
Γ ⊢ N : !t
subgoal 2 (ID 2669) is:
Γ ⊢ N : A
subgoal 3 (ID 2671) is:
Γ ⊢ N : !u
subgoal 4 (ID 2673) is:
Γ ⊢ N : Π (A), B
subgoal 5 (ID 2675) is:
Γ ⊢ N0 : B [ ← N]
subgoal 6 (ID 2677) is:
Γ ⊢ N : B
(dependent evars:)
inversion H1.5 subgoals, subgoal 1 (ID 2669)
Γ : Env
A : Term
v : nat
H : Γ ⊣
H0 : A ↓ v ⊂ Γ
N : Term
H1 : #v → N
============================
Γ ⊢ N : A
subgoal 2 (ID 2671) is:
Γ ⊢ N : !u
subgoal 3 (ID 2673) is:
Γ ⊢ N : Π (A), B
subgoal 4 (ID 2675) is:
Γ ⊢ N0 : B [ ← N]
subgoal 5 (ID 2677) is:
Γ ⊢ N : B
(dependent evars:)
inversion H1.4 subgoals, subgoal 1 (ID 2671)
Γ : Env
A : Term
B : Term
s : X.Sorts
t : X.Sorts
u : X.Sorts
H : Y.Rel s t u
H0 : Γ ⊢ A : !s
H1 : A :: Γ ⊢ B : !t
IHtyp1 : forall N : Term, A → N -> Γ ⊢ N : !s
IHtyp2 : forall N : Term, B → N -> A :: Γ ⊢ N : !t
N : Term
H2 : Π (A), B → N
============================
Γ ⊢ N : !u
subgoal 2 (ID 2673) is:
Γ ⊢ N : Π (A), B
subgoal 3 (ID 2675) is:
Γ ⊢ N0 : B [ ← N]
subgoal 4 (ID 2677) is:
Γ ⊢ N : B
(dependent evars:)
inversion H2; subst; clear H2. 5 subgoals, subgoal 1 (ID 3098)
Γ : Env
A : Term
B : Term
s : X.Sorts
t : X.Sorts
u : X.Sorts
H : Y.Rel s t u
H0 : Γ ⊢ A : !s
H1 : A :: Γ ⊢ B : !t
IHtyp1 : forall N : Term, A → N -> Γ ⊢ N : !s
IHtyp2 : forall N : Term, B → N -> A :: Γ ⊢ N : !t
B' : Term
H6 : B → B'
============================
Γ ⊢ Π (A), B' : !u
subgoal 2 (ID 3099) is:
Γ ⊢ Π (A'), B : !u
subgoal 3 (ID 2673) is:
Γ ⊢ N : Π (A), B
subgoal 4 (ID 2675) is:
Γ ⊢ N0 : B [ ← N]
subgoal 5 (ID 2677) is:
Γ ⊢ N : B
(dependent evars:)
econstructor; eauto. 4 subgoals, subgoal 1 (ID 3099)
Γ : Env
A : Term
B : Term
s : X.Sorts
t : X.Sorts
u : X.Sorts
H : Y.Rel s t u
H0 : Γ ⊢ A : !s
H1 : A :: Γ ⊢ B : !t
IHtyp1 : forall N : Term, A → N -> Γ ⊢ N : !s
IHtyp2 : forall N : Term, B → N -> A :: Γ ⊢ N : !t
A' : Term
H6 : A → A'
============================
Γ ⊢ Π (A'), B : !u
subgoal 2 (ID 2673) is:
Γ ⊢ N : Π (A), B
subgoal 3 (ID 2675) is:
Γ ⊢ N0 : B [ ← N]
subgoal 4 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using ,)
econstructor. 6 subgoals, subgoal 1 (ID 3125)
Γ : Env
A : Term
B : Term
s : X.Sorts
t : X.Sorts
u : X.Sorts
H : Y.Rel s t u
H0 : Γ ⊢ A : !s
H1 : A :: Γ ⊢ B : !t
IHtyp1 : forall N : Term, A → N -> Γ ⊢ N : !s
IHtyp2 : forall N : Term, B → N -> A :: Γ ⊢ N : !t
A' : Term
H6 : A → A'
============================
Y.Rel ?3123 ?3124 u
subgoal 2 (ID 3126) is:
Γ ⊢ A' : !?3123
subgoal 3 (ID 3127) is:
A' :: Γ ⊢ B : !?3124
subgoal 4 (ID 2673) is:
Γ ⊢ N : Π (A), B
subgoal 5 (ID 2675) is:
Γ ⊢ N0 : B [ ← N]
subgoal 6 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 open, ?3124 open,)
apply H. 5 subgoals, subgoal 1 (ID 3126)
Γ : Env
A : Term
B : Term
s : X.Sorts
t : X.Sorts
u : X.Sorts
H : Y.Rel s t u
H0 : Γ ⊢ A : !s
H1 : A :: Γ ⊢ B : !t
IHtyp1 : forall N : Term, A → N -> Γ ⊢ N : !s
IHtyp2 : forall N : Term, B → N -> A :: Γ ⊢ N : !t
A' : Term
H6 : A → A'
============================
Γ ⊢ A' : !s
subgoal 2 (ID 3127) is:
A' :: Γ ⊢ B : !t
subgoal 3 (ID 2673) is:
Γ ⊢ N : Π (A), B
subgoal 4 (ID 2675) is:
Γ ⊢ N0 : B [ ← N]
subgoal 5 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using ,)
intuition.4 subgoals, subgoal 1 (ID 3127)
Γ : Env
A : Term
B : Term
s : X.Sorts
t : X.Sorts
u : X.Sorts
H : Y.Rel s t u
H0 : Γ ⊢ A : !s
H1 : A :: Γ ⊢ B : !t
IHtyp1 : forall N : Term, A → N -> Γ ⊢ N : !s
IHtyp2 : forall N : Term, B → N -> A :: Γ ⊢ N : !t
A' : Term
H6 : A → A'
============================
A' :: Γ ⊢ B : !t
subgoal 2 (ID 2673) is:
Γ ⊢ N : Π (A), B
subgoal 3 (ID 2675) is:
Γ ⊢ N0 : B [ ← N]
subgoal 4 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using ,)
eapply Beta_env_sound. 6 subgoals, subgoal 1 (ID 3144)
Γ : Env
A : Term
B : Term
s : X.Sorts
t : X.Sorts
u : X.Sorts
H : Y.Rel s t u
H0 : Γ ⊢ A : !s
H1 : A :: Γ ⊢ B : !t
IHtyp1 : forall N : Term, A → N -> Γ ⊢ N : !s
IHtyp2 : forall N : Term, B → N -> A :: Γ ⊢ N : !t
A' : Term
H6 : A → A'
============================
?3143 ⊢ B : !t
subgoal 2 (ID 3145) is:
A' :: Γ ⊣
subgoal 3 (ID 3146) is:
?3143 →e (A' :: Γ)
subgoal 4 (ID 2673) is:
Γ ⊢ N : Π (A), B
subgoal 5 (ID 2675) is:
Γ ⊢ N0 : B [ ← N]
subgoal 6 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 open,)
apply H1. 5 subgoals, subgoal 1 (ID 3145)
Γ : Env
A : Term
B : Term
s : X.Sorts
t : X.Sorts
u : X.Sorts
H : Y.Rel s t u
H0 : Γ ⊢ A : !s
H1 : A :: Γ ⊢ B : !t
IHtyp1 : forall N : Term, A → N -> Γ ⊢ N : !s
IHtyp2 : forall N : Term, B → N -> A :: Γ ⊢ N : !t
A' : Term
H6 : A → A'
============================
A' :: Γ ⊣
subgoal 2 (ID 3146) is:
(A :: Γ) →e (A' :: Γ)
subgoal 3 (ID 2673) is:
Γ ⊢ N : Π (A), B
subgoal 4 (ID 2675) is:
Γ ⊢ N0 : B [ ← N]
subgoal 5 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using ,)
eauto. 4 subgoals, subgoal 1 (ID 3146)
Γ : Env
A : Term
B : Term
s : X.Sorts
t : X.Sorts
u : X.Sorts
H : Y.Rel s t u
H0 : Γ ⊢ A : !s
H1 : A :: Γ ⊢ B : !t
IHtyp1 : forall N : Term, A → N -> Γ ⊢ N : !s
IHtyp2 : forall N : Term, B → N -> A :: Γ ⊢ N : !t
A' : Term
H6 : A → A'
============================
(A :: Γ) →e (A' :: Γ)
subgoal 2 (ID 2673) is:
Γ ⊢ N : Π (A), B
subgoal 3 (ID 2675) is:
Γ ⊢ N0 : B [ ← N]
subgoal 4 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using ,)
intuition.3 subgoals, subgoal 1 (ID 2673)
Γ : Env
A : Term
B : Term
M : Term
s1 : X.Sorts
s2 : X.Sorts
s3 : X.Sorts
H : Y.Rel s1 s2 s3
H0 : Γ ⊢ A : !s1
H1 : A :: Γ ⊢ B : !s2
H2 : A :: Γ ⊢ M : B
IHtyp1 : forall N : Term, A → N -> Γ ⊢ N : !s1
IHtyp2 : forall N : Term, B → N -> A :: Γ ⊢ N : !s2
IHtyp3 : forall N : Term, M → N -> A :: Γ ⊢ N : B
N : Term
H3 : λ [A], M → N
============================
Γ ⊢ N : Π (A), B
subgoal 2 (ID 2675) is:
Γ ⊢ N0 : B [ ← N]
subgoal 3 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using ,)
inversion H3; subst; clear H3. 4 subgoals, subgoal 1 (ID 3349)
Γ : Env
A : Term
B : Term
M : Term
s1 : X.Sorts
s2 : X.Sorts
s3 : X.Sorts
H : Y.Rel s1 s2 s3
H0 : Γ ⊢ A : !s1
H1 : A :: Γ ⊢ B : !s2
H2 : A :: Γ ⊢ M : B
IHtyp1 : forall N : Term, A → N -> Γ ⊢ N : !s1
IHtyp2 : forall N : Term, B → N -> A :: Γ ⊢ N : !s2
IHtyp3 : forall N : Term, M → N -> A :: Γ ⊢ N : B
M' : Term
H7 : M → M'
============================
Γ ⊢ λ [A], M' : Π (A), B
subgoal 2 (ID 3350) is:
Γ ⊢ λ [A'], M : Π (A), B
subgoal 3 (ID 2675) is:
Γ ⊢ N0 : B [ ← N]
subgoal 4 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using ,)
eauto.3 subgoals, subgoal 1 (ID 3350)
Γ : Env
A : Term
B : Term
M : Term
s1 : X.Sorts
s2 : X.Sorts
s3 : X.Sorts
H : Y.Rel s1 s2 s3
H0 : Γ ⊢ A : !s1
H1 : A :: Γ ⊢ B : !s2
H2 : A :: Γ ⊢ M : B
IHtyp1 : forall N : Term, A → N -> Γ ⊢ N : !s1
IHtyp2 : forall N : Term, B → N -> A :: Γ ⊢ N : !s2
IHtyp3 : forall N : Term, M → N -> A :: Γ ⊢ N : B
A' : Term
H7 : A → A'
============================
Γ ⊢ λ [A'], M : Π (A), B
subgoal 2 (ID 2675) is:
Γ ⊢ N0 : B [ ← N]
subgoal 3 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using ,)
apply Cnv with ( Π (A'), B) s3. 5 subgoals, subgoal 1 (ID 5203)
Γ : Env
A : Term
B : Term
M : Term
s1 : X.Sorts
s2 : X.Sorts
s3 : X.Sorts
H : Y.Rel s1 s2 s3
H0 : Γ ⊢ A : !s1
H1 : A :: Γ ⊢ B : !s2
H2 : A :: Γ ⊢ M : B
IHtyp1 : forall N : Term, A → N -> Γ ⊢ N : !s1
IHtyp2 : forall N : Term, B → N -> A :: Γ ⊢ N : !s2
IHtyp3 : forall N : Term, M → N -> A :: Γ ⊢ N : B
A' : Term
H7 : A → A'
============================
Π (A'), B ≡ Π (A), B
subgoal 2 (ID 5204) is:
Γ ⊢ λ [A'], M : Π (A'), B
subgoal 3 (ID 5205) is:
Γ ⊢ Π (A), B : !s3
subgoal 4 (ID 2675) is:
Γ ⊢ N0 : B [ ← N]
subgoal 5 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using ,)
eauto.4 subgoals, subgoal 1 (ID 5204)
Γ : Env
A : Term
B : Term
M : Term
s1 : X.Sorts
s2 : X.Sorts
s3 : X.Sorts
H : Y.Rel s1 s2 s3
H0 : Γ ⊢ A : !s1
H1 : A :: Γ ⊢ B : !s2
H2 : A :: Γ ⊢ M : B
IHtyp1 : forall N : Term, A → N -> Γ ⊢ N : !s1
IHtyp2 : forall N : Term, B → N -> A :: Γ ⊢ N : !s2
IHtyp3 : forall N : Term, M → N -> A :: Γ ⊢ N : B
A' : Term
H7 : A → A'
============================
Γ ⊢ λ [A'], M : Π (A'), B
subgoal 2 (ID 5205) is:
Γ ⊢ Π (A), B : !s3
subgoal 3 (ID 2675) is:
Γ ⊢ N0 : B [ ← N]
subgoal 4 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using ,)
econstructor. 7 subgoals, subgoal 1 (ID 5454)
Γ : Env
A : Term
B : Term
M : Term
s1 : X.Sorts
s2 : X.Sorts
s3 : X.Sorts
H : Y.Rel s1 s2 s3
H0 : Γ ⊢ A : !s1
H1 : A :: Γ ⊢ B : !s2
H2 : A :: Γ ⊢ M : B
IHtyp1 : forall N : Term, A → N -> Γ ⊢ N : !s1
IHtyp2 : forall N : Term, B → N -> A :: Γ ⊢ N : !s2
IHtyp3 : forall N : Term, M → N -> A :: Γ ⊢ N : B
A' : Term
H7 : A → A'
============================
Y.Rel ?5451 ?5452 ?5453
subgoal 2 (ID 5455) is:
Γ ⊢ A' : !?5451
subgoal 3 (ID 5456) is:
A' :: Γ ⊢ B : !?5452
subgoal 4 (ID 5457) is:
A' :: Γ ⊢ M : B
subgoal 5 (ID 5205) is:
Γ ⊢ Π (A), B : !s3
subgoal 6 (ID 2675) is:
Γ ⊢ N0 : B [ ← N]
subgoal 7 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 open, ?5452 open, ?5453 open,)
apply H. 6 subgoals, subgoal 1 (ID 5455)
Γ : Env
A : Term
B : Term
M : Term
s1 : X.Sorts
s2 : X.Sorts
s3 : X.Sorts
H : Y.Rel s1 s2 s3
H0 : Γ ⊢ A : !s1
H1 : A :: Γ ⊢ B : !s2
H2 : A :: Γ ⊢ M : B
IHtyp1 : forall N : Term, A → N -> Γ ⊢ N : !s1
IHtyp2 : forall N : Term, B → N -> A :: Γ ⊢ N : !s2
IHtyp3 : forall N : Term, M → N -> A :: Γ ⊢ N : B
A' : Term
H7 : A → A'
============================
Γ ⊢ A' : !s1
subgoal 2 (ID 5456) is:
A' :: Γ ⊢ B : !s2
subgoal 3 (ID 5457) is:
A' :: Γ ⊢ M : B
subgoal 4 (ID 5205) is:
Γ ⊢ Π (A), B : !s3
subgoal 5 (ID 2675) is:
Γ ⊢ N0 : B [ ← N]
subgoal 6 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using ,)
eauto.5 subgoals, subgoal 1 (ID 5456)
Γ : Env
A : Term
B : Term
M : Term
s1 : X.Sorts
s2 : X.Sorts
s3 : X.Sorts
H : Y.Rel s1 s2 s3
H0 : Γ ⊢ A : !s1
H1 : A :: Γ ⊢ B : !s2
H2 : A :: Γ ⊢ M : B
IHtyp1 : forall N : Term, A → N -> Γ ⊢ N : !s1
IHtyp2 : forall N : Term, B → N -> A :: Γ ⊢ N : !s2
IHtyp3 : forall N : Term, M → N -> A :: Γ ⊢ N : B
A' : Term
H7 : A → A'
============================
A' :: Γ ⊢ B : !s2
subgoal 2 (ID 5457) is:
A' :: Γ ⊢ M : B
subgoal 3 (ID 5205) is:
Γ ⊢ Π (A), B : !s3
subgoal 4 (ID 2675) is:
Γ ⊢ N0 : B [ ← N]
subgoal 5 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using ,)
eapply Beta_env_sound. 7 subgoals, subgoal 1 (ID 5465)
Γ : Env
A : Term
B : Term
M : Term
s1 : X.Sorts
s2 : X.Sorts
s3 : X.Sorts
H : Y.Rel s1 s2 s3
H0 : Γ ⊢ A : !s1
H1 : A :: Γ ⊢ B : !s2
H2 : A :: Γ ⊢ M : B
IHtyp1 : forall N : Term, A → N -> Γ ⊢ N : !s1
IHtyp2 : forall N : Term, B → N -> A :: Γ ⊢ N : !s2
IHtyp3 : forall N : Term, M → N -> A :: Γ ⊢ N : B
A' : Term
H7 : A → A'
============================
?5464 ⊢ B : !s2
subgoal 2 (ID 5466) is:
A' :: Γ ⊣
subgoal 3 (ID 5467) is:
?5464 →e (A' :: Γ)
subgoal 4 (ID 5457) is:
A' :: Γ ⊢ M : B
subgoal 5 (ID 5205) is:
Γ ⊢ Π (A), B : !s3
subgoal 6 (ID 2675) is:
Γ ⊢ N0 : B [ ← N]
subgoal 7 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using , ?5464 open,)
apply H1. 6 subgoals, subgoal 1 (ID 5466)
Γ : Env
A : Term
B : Term
M : Term
s1 : X.Sorts
s2 : X.Sorts
s3 : X.Sorts
H : Y.Rel s1 s2 s3
H0 : Γ ⊢ A : !s1
H1 : A :: Γ ⊢ B : !s2
H2 : A :: Γ ⊢ M : B
IHtyp1 : forall N : Term, A → N -> Γ ⊢ N : !s1
IHtyp2 : forall N : Term, B → N -> A :: Γ ⊢ N : !s2
IHtyp3 : forall N : Term, M → N -> A :: Γ ⊢ N : B
A' : Term
H7 : A → A'
============================
A' :: Γ ⊣
subgoal 2 (ID 5467) is:
(A :: Γ) →e (A' :: Γ)
subgoal 3 (ID 5457) is:
A' :: Γ ⊢ M : B
subgoal 4 (ID 5205) is:
Γ ⊢ Π (A), B : !s3
subgoal 5 (ID 2675) is:
Γ ⊢ N0 : B [ ← N]
subgoal 6 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using , ?5464 using ,)
econstructor. 6 subgoals, subgoal 1 (ID 5471)
Γ : Env
A : Term
B : Term
M : Term
s1 : X.Sorts
s2 : X.Sorts
s3 : X.Sorts
H : Y.Rel s1 s2 s3
H0 : Γ ⊢ A : !s1
H1 : A :: Γ ⊢ B : !s2
H2 : A :: Γ ⊢ M : B
IHtyp1 : forall N : Term, A → N -> Γ ⊢ N : !s1
IHtyp2 : forall N : Term, B → N -> A :: Γ ⊢ N : !s2
IHtyp3 : forall N : Term, M → N -> A :: Γ ⊢ N : B
A' : Term
H7 : A → A'
============================
Γ ⊢ A' : !?5470
subgoal 2 (ID 5467) is:
(A :: Γ) →e (A' :: Γ)
subgoal 3 (ID 5457) is:
A' :: Γ ⊢ M : B
subgoal 4 (ID 5205) is:
Γ ⊢ Π (A), B : !s3
subgoal 5 (ID 2675) is:
Γ ⊢ N0 : B [ ← N]
subgoal 6 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using , ?5464 using , ?5470 open,)
eauto. 5 subgoals, subgoal 1 (ID 5467)
Γ : Env
A : Term
B : Term
M : Term
s1 : X.Sorts
s2 : X.Sorts
s3 : X.Sorts
H : Y.Rel s1 s2 s3
H0 : Γ ⊢ A : !s1
H1 : A :: Γ ⊢ B : !s2
H2 : A :: Γ ⊢ M : B
IHtyp1 : forall N : Term, A → N -> Γ ⊢ N : !s1
IHtyp2 : forall N : Term, B → N -> A :: Γ ⊢ N : !s2
IHtyp3 : forall N : Term, M → N -> A :: Γ ⊢ N : B
A' : Term
H7 : A → A'
============================
(A :: Γ) →e (A' :: Γ)
subgoal 2 (ID 5457) is:
A' :: Γ ⊢ M : B
subgoal 3 (ID 5205) is:
Γ ⊢ Π (A), B : !s3
subgoal 4 (ID 2675) is:
Γ ⊢ N0 : B [ ← N]
subgoal 5 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using , ?5464 using , ?5470 using ,)
intuition.4 subgoals, subgoal 1 (ID 5457)
Γ : Env
A : Term
B : Term
M : Term
s1 : X.Sorts
s2 : X.Sorts
s3 : X.Sorts
H : Y.Rel s1 s2 s3
H0 : Γ ⊢ A : !s1
H1 : A :: Γ ⊢ B : !s2
H2 : A :: Γ ⊢ M : B
IHtyp1 : forall N : Term, A → N -> Γ ⊢ N : !s1
IHtyp2 : forall N : Term, B → N -> A :: Γ ⊢ N : !s2
IHtyp3 : forall N : Term, M → N -> A :: Γ ⊢ N : B
A' : Term
H7 : A → A'
============================
A' :: Γ ⊢ M : B
subgoal 2 (ID 5205) is:
Γ ⊢ Π (A), B : !s3
subgoal 3 (ID 2675) is:
Γ ⊢ N0 : B [ ← N]
subgoal 4 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using , ?5464 using , ?5470 using ,)
eapply Beta_env_sound. 6 subgoals, subgoal 1 (ID 5497)
Γ : Env
A : Term
B : Term
M : Term
s1 : X.Sorts
s2 : X.Sorts
s3 : X.Sorts
H : Y.Rel s1 s2 s3
H0 : Γ ⊢ A : !s1
H1 : A :: Γ ⊢ B : !s2
H2 : A :: Γ ⊢ M : B
IHtyp1 : forall N : Term, A → N -> Γ ⊢ N : !s1
IHtyp2 : forall N : Term, B → N -> A :: Γ ⊢ N : !s2
IHtyp3 : forall N : Term, M → N -> A :: Γ ⊢ N : B
A' : Term
H7 : A → A'
============================
?5496 ⊢ M : B
subgoal 2 (ID 5498) is:
A' :: Γ ⊣
subgoal 3 (ID 5499) is:
?5496 →e (A' :: Γ)
subgoal 4 (ID 5205) is:
Γ ⊢ Π (A), B : !s3
subgoal 5 (ID 2675) is:
Γ ⊢ N0 : B [ ← N]
subgoal 6 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using , ?5464 using , ?5470 using , ?5496 open,)
apply H2. 5 subgoals, subgoal 1 (ID 5498)
Γ : Env
A : Term
B : Term
M : Term
s1 : X.Sorts
s2 : X.Sorts
s3 : X.Sorts
H : Y.Rel s1 s2 s3
H0 : Γ ⊢ A : !s1
H1 : A :: Γ ⊢ B : !s2
H2 : A :: Γ ⊢ M : B
IHtyp1 : forall N : Term, A → N -> Γ ⊢ N : !s1
IHtyp2 : forall N : Term, B → N -> A :: Γ ⊢ N : !s2
IHtyp3 : forall N : Term, M → N -> A :: Γ ⊢ N : B
A' : Term
H7 : A → A'
============================
A' :: Γ ⊣
subgoal 2 (ID 5499) is:
(A :: Γ) →e (A' :: Γ)
subgoal 3 (ID 5205) is:
Γ ⊢ Π (A), B : !s3
subgoal 4 (ID 2675) is:
Γ ⊢ N0 : B [ ← N]
subgoal 5 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using , ?5464 using , ?5470 using , ?5496 using ,)
econstructor. 5 subgoals, subgoal 1 (ID 5503)
Γ : Env
A : Term
B : Term
M : Term
s1 : X.Sorts
s2 : X.Sorts
s3 : X.Sorts
H : Y.Rel s1 s2 s3
H0 : Γ ⊢ A : !s1
H1 : A :: Γ ⊢ B : !s2
H2 : A :: Γ ⊢ M : B
IHtyp1 : forall N : Term, A → N -> Γ ⊢ N : !s1
IHtyp2 : forall N : Term, B → N -> A :: Γ ⊢ N : !s2
IHtyp3 : forall N : Term, M → N -> A :: Γ ⊢ N : B
A' : Term
H7 : A → A'
============================
Γ ⊢ A' : !?5502
subgoal 2 (ID 5499) is:
(A :: Γ) →e (A' :: Γ)
subgoal 3 (ID 5205) is:
Γ ⊢ Π (A), B : !s3
subgoal 4 (ID 2675) is:
Γ ⊢ N0 : B [ ← N]
subgoal 5 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using , ?5464 using , ?5470 using , ?5496 using , ?5502 open,)
eauto. 4 subgoals, subgoal 1 (ID 5499)
Γ : Env
A : Term
B : Term
M : Term
s1 : X.Sorts
s2 : X.Sorts
s3 : X.Sorts
H : Y.Rel s1 s2 s3
H0 : Γ ⊢ A : !s1
H1 : A :: Γ ⊢ B : !s2
H2 : A :: Γ ⊢ M : B
IHtyp1 : forall N : Term, A → N -> Γ ⊢ N : !s1
IHtyp2 : forall N : Term, B → N -> A :: Γ ⊢ N : !s2
IHtyp3 : forall N : Term, M → N -> A :: Γ ⊢ N : B
A' : Term
H7 : A → A'
============================
(A :: Γ) →e (A' :: Γ)
subgoal 2 (ID 5205) is:
Γ ⊢ Π (A), B : !s3
subgoal 3 (ID 2675) is:
Γ ⊢ N0 : B [ ← N]
subgoal 4 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using , ?5464 using , ?5470 using , ?5496 using , ?5502 using ,)
intuition.3 subgoals, subgoal 1 (ID 5205)
Γ : Env
A : Term
B : Term
M : Term
s1 : X.Sorts
s2 : X.Sorts
s3 : X.Sorts
H : Y.Rel s1 s2 s3
H0 : Γ ⊢ A : !s1
H1 : A :: Γ ⊢ B : !s2
H2 : A :: Γ ⊢ M : B
IHtyp1 : forall N : Term, A → N -> Γ ⊢ N : !s1
IHtyp2 : forall N : Term, B → N -> A :: Γ ⊢ N : !s2
IHtyp3 : forall N : Term, M → N -> A :: Γ ⊢ N : B
A' : Term
H7 : A → A'
============================
Γ ⊢ Π (A), B : !s3
subgoal 2 (ID 2675) is:
Γ ⊢ N0 : B [ ← N]
subgoal 3 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using , ?5464 using , ?5470 using , ?5496 using , ?5502 using ,)
econstructor; eauto.2 subgoals, subgoal 1 (ID 2675)
Γ : Env
M : Term
N : Term
A : Term
B : Term
H : Γ ⊢ M : Π (A), B
H0 : Γ ⊢ N : A
IHtyp1 : forall N : Term, M → N -> Γ ⊢ N : Π (A), B
IHtyp2 : forall N0 : Term, N → N0 -> Γ ⊢ N0 : A
N0 : Term
H1 : M · N → N0
============================
Γ ⊢ N0 : B [ ← N]
subgoal 2 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using , ?5464 using , ?5470 using , ?5496 using , ?5502 using , ?5531 using , ?5532 using ,)
inversion H1; subst; clear H1.4 subgoals, subgoal 1 (ID 5751)
Γ : Env
N : Term
A : Term
B : Term
H0 : Γ ⊢ N : A
IHtyp2 : forall N0 : Term, N → N0 -> Γ ⊢ N0 : A
A0 : Term
M0 : Term
H : Γ ⊢ λ [A0], M0 : Π (A), B
IHtyp1 : forall N : Term, λ [A0], M0 → N -> Γ ⊢ N : Π (A), B
============================
Γ ⊢ M0 [ ← N] : B [ ← N]
subgoal 2 (ID 5752) is:
Γ ⊢ M' · N : B [ ← N]
subgoal 3 (ID 5753) is:
Γ ⊢ M · N' : B [ ← N]
subgoal 4 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using , ?5464 using , ?5470 using , ?5496 using , ?5502 using , ?5531 using , ?5532 using ,)
assert (exists u, Γ ⊢ Π(A),B : !u). 5 subgoals, subgoal 1 (ID 5755)
Γ : Env
N : Term
A : Term
B : Term
H0 : Γ ⊢ N : A
IHtyp2 : forall N0 : Term, N → N0 -> Γ ⊢ N0 : A
A0 : Term
M0 : Term
H : Γ ⊢ λ [A0], M0 : Π (A), B
IHtyp1 : forall N : Term, λ [A0], M0 → N -> Γ ⊢ N : Π (A), B
============================
exists u : X.Sorts, Γ ⊢ Π (A), B : !u
subgoal 2 (ID 5756) is:
Γ ⊢ M0 [ ← N] : B [ ← N]
subgoal 3 (ID 5752) is:
Γ ⊢ M' · N : B [ ← N]
subgoal 4 (ID 5753) is:
Γ ⊢ M · N' : B [ ← N]
subgoal 5 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using , ?5464 using , ?5470 using , ?5496 using , ?5502 using , ?5531 using , ?5532 using ,)
apply TypeCorrect in H.5 subgoals, subgoal 1 (ID 5758)
Γ : Env
N : Term
A : Term
B : Term
H0 : Γ ⊢ N : A
IHtyp2 : forall N0 : Term, N → N0 -> Γ ⊢ N0 : A
A0 : Term
M0 : Term
H : (exists s : X.Sorts, Π (A), B = !s) \/
(exists s : X.Sorts, Γ ⊢ Π (A), B : !s)
IHtyp1 : forall N : Term, λ [A0], M0 → N -> Γ ⊢ N : Π (A), B
============================
exists u : X.Sorts, Γ ⊢ Π (A), B : !u
subgoal 2 (ID 5756) is:
Γ ⊢ M0 [ ← N] : B [ ← N]
subgoal 3 (ID 5752) is:
Γ ⊢ M' · N : B [ ← N]
subgoal 4 (ID 5753) is:
Γ ⊢ M · N' : B [ ← N]
subgoal 5 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using , ?5464 using , ?5470 using , ?5496 using , ?5502 using , ?5531 using , ?5532 using ,)
destruct H. 6 subgoals, subgoal 1 (ID 5764)
Γ : Env
N : Term
A : Term
B : Term
H0 : Γ ⊢ N : A
IHtyp2 : forall N0 : Term, N → N0 -> Γ ⊢ N0 : A
A0 : Term
M0 : Term
H : exists s : X.Sorts, Π (A), B = !s
IHtyp1 : forall N : Term, λ [A0], M0 → N -> Γ ⊢ N : Π (A), B
============================
exists u : X.Sorts, Γ ⊢ Π (A), B : !u
subgoal 2 (ID 5766) is:
exists u : X.Sorts, Γ ⊢ Π (A), B : !u
subgoal 3 (ID 5756) is:
Γ ⊢ M0 [ ← N] : B [ ← N]
subgoal 4 (ID 5752) is:
Γ ⊢ M' · N : B [ ← N]
subgoal 5 (ID 5753) is:
Γ ⊢ M · N' : B [ ← N]
subgoal 6 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using , ?5464 using , ?5470 using , ?5496 using , ?5502 using , ?5531 using , ?5532 using ,)
destruct H; discriminate. 5 subgoals, subgoal 1 (ID 5766)
Γ : Env
N : Term
A : Term
B : Term
H0 : Γ ⊢ N : A
IHtyp2 : forall N0 : Term, N → N0 -> Γ ⊢ N0 : A
A0 : Term
M0 : Term
H : exists s : X.Sorts, Γ ⊢ Π (A), B : !s
IHtyp1 : forall N : Term, λ [A0], M0 → N -> Γ ⊢ N : Π (A), B
============================
exists u : X.Sorts, Γ ⊢ Π (A), B : !u
subgoal 2 (ID 5756) is:
Γ ⊢ M0 [ ← N] : B [ ← N]
subgoal 3 (ID 5752) is:
Γ ⊢ M' · N : B [ ← N]
subgoal 4 (ID 5753) is:
Γ ⊢ M · N' : B [ ← N]
subgoal 5 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using , ?5464 using , ?5470 using , ?5496 using , ?5502 using , ?5531 using , ?5532 using ,)
trivial.4 subgoals, subgoal 1 (ID 5756)
Γ : Env
N : Term
A : Term
B : Term
H0 : Γ ⊢ N : A
IHtyp2 : forall N0 : Term, N → N0 -> Γ ⊢ N0 : A
A0 : Term
M0 : Term
H : Γ ⊢ λ [A0], M0 : Π (A), B
IHtyp1 : forall N : Term, λ [A0], M0 → N -> Γ ⊢ N : Π (A), B
H1 : exists u : X.Sorts, Γ ⊢ Π (A), B : !u
============================
Γ ⊢ M0 [ ← N] : B [ ← N]
subgoal 2 (ID 5752) is:
Γ ⊢ M' · N : B [ ← N]
subgoal 3 (ID 5753) is:
Γ ⊢ M · N' : B [ ← N]
subgoal 4 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using , ?5464 using , ?5470 using , ?5496 using , ?5502 using , ?5531 using , ?5532 using ,)
destruct H1. 4 subgoals, subgoal 1 (ID 5781)
Γ : Env
N : Term
A : Term
B : Term
H0 : Γ ⊢ N : A
IHtyp2 : forall N0 : Term, N → N0 -> Γ ⊢ N0 : A
A0 : Term
M0 : Term
H : Γ ⊢ λ [A0], M0 : Π (A), B
IHtyp1 : forall N : Term, λ [A0], M0 → N -> Γ ⊢ N : Π (A), B
x : X.Sorts
H1 : Γ ⊢ Π (A), B : !x
============================
Γ ⊢ M0 [ ← N] : B [ ← N]
subgoal 2 (ID 5752) is:
Γ ⊢ M' · N : B [ ← N]
subgoal 3 (ID 5753) is:
Γ ⊢ M · N' : B [ ← N]
subgoal 4 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using , ?5464 using , ?5470 using , ?5496 using , ?5502 using , ?5531 using , ?5532 using ,)
apply gen_pi in H1 as (s & t & u & h); decompose [and] h; clear h.4 subgoals, subgoal 1 (ID 5813)
Γ : Env
N : Term
A : Term
B : Term
H0 : Γ ⊢ N : A
IHtyp2 : forall N0 : Term, N → N0 -> Γ ⊢ N0 : A
A0 : Term
M0 : Term
H : Γ ⊢ λ [A0], M0 : Π (A), B
IHtyp1 : forall N : Term, λ [A0], M0 → N -> Γ ⊢ N : Π (A), B
x : X.Sorts
s : X.Sorts
t : X.Sorts
u : X.Sorts
H1 : !x ≡ !u
H3 : Y.Rel s t u
H2 : Γ ⊢ A : !s
H5 : A :: Γ ⊢ B : !t
============================
Γ ⊢ M0 [ ← N] : B [ ← N]
subgoal 2 (ID 5752) is:
Γ ⊢ M' · N : B [ ← N]
subgoal 3 (ID 5753) is:
Γ ⊢ M · N' : B [ ← N]
subgoal 4 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using , ?5464 using , ?5470 using , ?5496 using , ?5502 using , ?5531 using , ?5532 using ,)
apply gen_la in H as (u1 & u2 & u3 & D & ? & ? & ? & ? & ?).4 subgoals, subgoal 1 (ID 5847)
Γ : Env
N : Term
A : Term
B : Term
H0 : Γ ⊢ N : A
IHtyp2 : forall N0 : Term, N → N0 -> Γ ⊢ N0 : A
A0 : Term
M0 : Term
IHtyp1 : forall N : Term, λ [A0], M0 → N -> Γ ⊢ N : Π (A), B
x : X.Sorts
s : X.Sorts
t : X.Sorts
u : X.Sorts
H1 : !x ≡ !u
H3 : Y.Rel s t u
H2 : Γ ⊢ A : !s
H5 : A :: Γ ⊢ B : !t
u1 : X.Sorts
u2 : X.Sorts
u3 : X.Sorts
D : Term
H : Π (A), B ≡ Π (A0), D
H4 : Y.Rel u1 u2 u3
H6 : Γ ⊢ A0 : !u1
H7 : A0 :: Γ ⊢ M0 : D
H8 : A0 :: Γ ⊢ D : !u2
============================
Γ ⊢ M0 [ ← N] : B [ ← N]
subgoal 2 (ID 5752) is:
Γ ⊢ M' · N : B [ ← N]
subgoal 3 (ID 5753) is:
Γ ⊢ M · N' : B [ ← N]
subgoal 4 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using , ?5464 using , ?5470 using , ?5496 using , ?5502 using , ?5531 using , ?5532 using ,)
apply PiInj in H as (? & ?).4 subgoals, subgoal 1 (ID 5853)
Γ : Env
N : Term
A : Term
B : Term
H0 : Γ ⊢ N : A
IHtyp2 : forall N0 : Term, N → N0 -> Γ ⊢ N0 : A
A0 : Term
M0 : Term
IHtyp1 : forall N : Term, λ [A0], M0 → N -> Γ ⊢ N : Π (A), B
x : X.Sorts
s : X.Sorts
t : X.Sorts
u : X.Sorts
H1 : !x ≡ !u
H3 : Y.Rel s t u
H2 : Γ ⊢ A : !s
H5 : A :: Γ ⊢ B : !t
u1 : X.Sorts
u2 : X.Sorts
u3 : X.Sorts
D : Term
H4 : Y.Rel u1 u2 u3
H6 : Γ ⊢ A0 : !u1
H7 : A0 :: Γ ⊢ M0 : D
H8 : A0 :: Γ ⊢ D : !u2
H : A ≡ A0
H9 : B ≡ D
============================
Γ ⊢ M0 [ ← N] : B [ ← N]
subgoal 2 (ID 5752) is:
Γ ⊢ M' · N : B [ ← N]
subgoal 3 (ID 5753) is:
Γ ⊢ M · N' : B [ ← N]
subgoal 4 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using , ?5464 using , ?5470 using , ?5496 using , ?5502 using , ?5531 using , ?5532 using ,)
eapply Cnv with (s := t). 6 subgoals, subgoal 1 (ID 5855)
Γ : Env
N : Term
A : Term
B : Term
H0 : Γ ⊢ N : A
IHtyp2 : forall N0 : Term, N → N0 -> Γ ⊢ N0 : A
A0 : Term
M0 : Term
IHtyp1 : forall N : Term, λ [A0], M0 → N -> Γ ⊢ N : Π (A), B
x : X.Sorts
s : X.Sorts
t : X.Sorts
u : X.Sorts
H1 : !x ≡ !u
H3 : Y.Rel s t u
H2 : Γ ⊢ A : !s
H5 : A :: Γ ⊢ B : !t
u1 : X.Sorts
u2 : X.Sorts
u3 : X.Sorts
D : Term
H4 : Y.Rel u1 u2 u3
H6 : Γ ⊢ A0 : !u1
H7 : A0 :: Γ ⊢ M0 : D
H8 : A0 :: Γ ⊢ D : !u2
H : A ≡ A0
H9 : B ≡ D
============================
?5854 ≡ B [ ← N]
subgoal 2 (ID 5856) is:
Γ ⊢ M0 [ ← N] : ?5854
subgoal 3 (ID 5857) is:
Γ ⊢ B [ ← N] : !t
subgoal 4 (ID 5752) is:
Γ ⊢ M' · N : B [ ← N]
subgoal 5 (ID 5753) is:
Γ ⊢ M · N' : B [ ← N]
subgoal 6 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using , ?5464 using , ?5470 using , ?5496 using , ?5502 using , ?5531 using , ?5532 using , ?5854 open,)
eapply Betac_subst2. 6 subgoals, subgoal 1 (ID 5859)
Γ : Env
N : Term
A : Term
B : Term
H0 : Γ ⊢ N : A
IHtyp2 : forall N0 : Term, N → N0 -> Γ ⊢ N0 : A
A0 : Term
M0 : Term
IHtyp1 : forall N : Term, λ [A0], M0 → N -> Γ ⊢ N : Π (A), B
x : X.Sorts
s : X.Sorts
t : X.Sorts
u : X.Sorts
H1 : !x ≡ !u
H3 : Y.Rel s t u
H2 : Γ ⊢ A : !s
H5 : A :: Γ ⊢ B : !t
u1 : X.Sorts
u2 : X.Sorts
u3 : X.Sorts
D : Term
H4 : Y.Rel u1 u2 u3
H6 : Γ ⊢ A0 : !u1
H7 : A0 :: Γ ⊢ M0 : D
H8 : A0 :: Γ ⊢ D : !u2
H : A ≡ A0
H9 : B ≡ D
============================
?5858 ≡ B
subgoal 2 (ID 5856) is:
Γ ⊢ M0 [ ← N] : ?5858 [ ← N]
subgoal 3 (ID 5857) is:
Γ ⊢ B [ ← N] : !t
subgoal 4 (ID 5752) is:
Γ ⊢ M' · N : B [ ← N]
subgoal 5 (ID 5753) is:
Γ ⊢ M · N' : B [ ← N]
subgoal 6 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using , ?5464 using , ?5470 using , ?5496 using , ?5502 using , ?5531 using , ?5532 using , ?5854 using ?5858 , ?5858 open,)
apply Betac_sym. 6 subgoals, subgoal 1 (ID 5860)
Γ : Env
N : Term
A : Term
B : Term
H0 : Γ ⊢ N : A
IHtyp2 : forall N0 : Term, N → N0 -> Γ ⊢ N0 : A
A0 : Term
M0 : Term
IHtyp1 : forall N : Term, λ [A0], M0 → N -> Γ ⊢ N : Π (A), B
x : X.Sorts
s : X.Sorts
t : X.Sorts
u : X.Sorts
H1 : !x ≡ !u
H3 : Y.Rel s t u
H2 : Γ ⊢ A : !s
H5 : A :: Γ ⊢ B : !t
u1 : X.Sorts
u2 : X.Sorts
u3 : X.Sorts
D : Term
H4 : Y.Rel u1 u2 u3
H6 : Γ ⊢ A0 : !u1
H7 : A0 :: Γ ⊢ M0 : D
H8 : A0 :: Γ ⊢ D : !u2
H : A ≡ A0
H9 : B ≡ D
============================
B ≡ ?5858
subgoal 2 (ID 5856) is:
Γ ⊢ M0 [ ← N] : ?5858 [ ← N]
subgoal 3 (ID 5857) is:
Γ ⊢ B [ ← N] : !t
subgoal 4 (ID 5752) is:
Γ ⊢ M' · N : B [ ← N]
subgoal 5 (ID 5753) is:
Γ ⊢ M · N' : B [ ← N]
subgoal 6 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using , ?5464 using , ?5470 using , ?5496 using , ?5502 using , ?5531 using , ?5532 using , ?5854 using ?5858 , ?5858 open,)
apply H9.5 subgoals, subgoal 1 (ID 5856)
Γ : Env
N : Term
A : Term
B : Term
H0 : Γ ⊢ N : A
IHtyp2 : forall N0 : Term, N → N0 -> Γ ⊢ N0 : A
A0 : Term
M0 : Term
IHtyp1 : forall N : Term, λ [A0], M0 → N -> Γ ⊢ N : Π (A), B
x : X.Sorts
s : X.Sorts
t : X.Sorts
u : X.Sorts
H1 : !x ≡ !u
H3 : Y.Rel s t u
H2 : Γ ⊢ A : !s
H5 : A :: Γ ⊢ B : !t
u1 : X.Sorts
u2 : X.Sorts
u3 : X.Sorts
D : Term
H4 : Y.Rel u1 u2 u3
H6 : Γ ⊢ A0 : !u1
H7 : A0 :: Γ ⊢ M0 : D
H8 : A0 :: Γ ⊢ D : !u2
H : A ≡ A0
H9 : B ≡ D
============================
Γ ⊢ M0 [ ← N] : D [ ← N]
subgoal 2 (ID 5857) is:
Γ ⊢ B [ ← N] : !t
subgoal 3 (ID 5752) is:
Γ ⊢ M' · N : B [ ← N]
subgoal 4 (ID 5753) is:
Γ ⊢ M · N' : B [ ← N]
subgoal 5 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using , ?5464 using , ?5470 using , ?5496 using , ?5502 using , ?5531 using , ?5532 using , ?5854 using ?5858 , ?5858 using ,)
eapply substitution. 8 subgoals, subgoal 1 (ID 5873)
Γ : Env
N : Term
A : Term
B : Term
H0 : Γ ⊢ N : A
IHtyp2 : forall N0 : Term, N → N0 -> Γ ⊢ N0 : A
A0 : Term
M0 : Term
IHtyp1 : forall N : Term, λ [A0], M0 → N -> Γ ⊢ N : Π (A), B
x : X.Sorts
s : X.Sorts
t : X.Sorts
u : X.Sorts
H1 : !x ≡ !u
H3 : Y.Rel s t u
H2 : Γ ⊢ A : !s
H5 : A :: Γ ⊢ B : !t
u1 : X.Sorts
u2 : X.Sorts
u3 : X.Sorts
D : Term
H4 : Y.Rel u1 u2 u3
H6 : Γ ⊢ A0 : !u1
H7 : A0 :: Γ ⊢ M0 : D
H8 : A0 :: Γ ⊢ D : !u2
H : A ≡ A0
H9 : B ≡ D
============================
?5872 ⊢ M0 : D
subgoal 2 (ID 5876) is:
?5874 ⊢ N : ?5875
subgoal 3 (ID 5877) is:
sub_in_env ?5874 N ?5875 0 ?5872 Γ
subgoal 4 (ID 5878) is:
?5872 ⊣
subgoal 5 (ID 5857) is:
Γ ⊢ B [ ← N] : !t
subgoal 6 (ID 5752) is:
Γ ⊢ M' · N : B [ ← N]
subgoal 7 (ID 5753) is:
Γ ⊢ M · N' : B [ ← N]
subgoal 8 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using , ?5464 using , ?5470 using , ?5496 using , ?5502 using , ?5531 using , ?5532 using , ?5854 using ?5858 , ?5858 using , ?5865 using ?5872 , ?5866 using ?5874 , ?5867 using ?5875 , ?5872 open, ?5874 open, ?5875 open,)
apply H7. 7 subgoals, subgoal 1 (ID 5876)
Γ : Env
N : Term
A : Term
B : Term
H0 : Γ ⊢ N : A
IHtyp2 : forall N0 : Term, N → N0 -> Γ ⊢ N0 : A
A0 : Term
M0 : Term
IHtyp1 : forall N : Term, λ [A0], M0 → N -> Γ ⊢ N : Π (A), B
x : X.Sorts
s : X.Sorts
t : X.Sorts
u : X.Sorts
H1 : !x ≡ !u
H3 : Y.Rel s t u
H2 : Γ ⊢ A : !s
H5 : A :: Γ ⊢ B : !t
u1 : X.Sorts
u2 : X.Sorts
u3 : X.Sorts
D : Term
H4 : Y.Rel u1 u2 u3
H6 : Γ ⊢ A0 : !u1
H7 : A0 :: Γ ⊢ M0 : D
H8 : A0 :: Γ ⊢ D : !u2
H : A ≡ A0
H9 : B ≡ D
============================
?5874 ⊢ N : ?5875
subgoal 2 (ID 5877) is:
sub_in_env ?5874 N ?5875 0 (A0 :: Γ) Γ
subgoal 3 (ID 5878) is:
A0 :: Γ ⊣
subgoal 4 (ID 5857) is:
Γ ⊢ B [ ← N] : !t
subgoal 5 (ID 5752) is:
Γ ⊢ M' · N : B [ ← N]
subgoal 6 (ID 5753) is:
Γ ⊢ M · N' : B [ ← N]
subgoal 7 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using , ?5464 using , ?5470 using , ?5496 using , ?5502 using , ?5531 using , ?5532 using , ?5854 using ?5858 , ?5858 using , ?5865 using ?5872 , ?5866 using ?5874 , ?5867 using ?5875 , ?5872 using , ?5874 open, ?5875 open,)
eapply Cnv. 9 subgoals, subgoal 1 (ID 5881)
Γ : Env
N : Term
A : Term
B : Term
H0 : Γ ⊢ N : A
IHtyp2 : forall N0 : Term, N → N0 -> Γ ⊢ N0 : A
A0 : Term
M0 : Term
IHtyp1 : forall N : Term, λ [A0], M0 → N -> Γ ⊢ N : Π (A), B
x : X.Sorts
s : X.Sorts
t : X.Sorts
u : X.Sorts
H1 : !x ≡ !u
H3 : Y.Rel s t u
H2 : Γ ⊢ A : !s
H5 : A :: Γ ⊢ B : !t
u1 : X.Sorts
u2 : X.Sorts
u3 : X.Sorts
D : Term
H4 : Y.Rel u1 u2 u3
H6 : Γ ⊢ A0 : !u1
H7 : A0 :: Γ ⊢ M0 : D
H8 : A0 :: Γ ⊢ D : !u2
H : A ≡ A0
H9 : B ≡ D
============================
?5879 ≡ ?5875
subgoal 2 (ID 5882) is:
?5874 ⊢ N : ?5879
subgoal 3 (ID 5883) is:
?5874 ⊢ ?5875 : !?5880
subgoal 4 (ID 5877) is:
sub_in_env ?5874 N ?5875 0 (A0 :: Γ) Γ
subgoal 5 (ID 5878) is:
A0 :: Γ ⊣
subgoal 6 (ID 5857) is:
Γ ⊢ B [ ← N] : !t
subgoal 7 (ID 5752) is:
Γ ⊢ M' · N : B [ ← N]
subgoal 8 (ID 5753) is:
Γ ⊢ M · N' : B [ ← N]
subgoal 9 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using , ?5464 using , ?5470 using , ?5496 using , ?5502 using , ?5531 using , ?5532 using , ?5854 using ?5858 , ?5858 using , ?5865 using ?5872 , ?5866 using ?5874 , ?5867 using ?5875 , ?5872 using , ?5874 open, ?5875 open, ?5879 open, ?5880 open,)
apply H. 8 subgoals, subgoal 1 (ID 5882)
Γ : Env
N : Term
A : Term
B : Term
H0 : Γ ⊢ N : A
IHtyp2 : forall N0 : Term, N → N0 -> Γ ⊢ N0 : A
A0 : Term
M0 : Term
IHtyp1 : forall N : Term, λ [A0], M0 → N -> Γ ⊢ N : Π (A), B
x : X.Sorts
s : X.Sorts
t : X.Sorts
u : X.Sorts
H1 : !x ≡ !u
H3 : Y.Rel s t u
H2 : Γ ⊢ A : !s
H5 : A :: Γ ⊢ B : !t
u1 : X.Sorts
u2 : X.Sorts
u3 : X.Sorts
D : Term
H4 : Y.Rel u1 u2 u3
H6 : Γ ⊢ A0 : !u1
H7 : A0 :: Γ ⊢ M0 : D
H8 : A0 :: Γ ⊢ D : !u2
H : A ≡ A0
H9 : B ≡ D
============================
?5874 ⊢ N : A
subgoal 2 (ID 5883) is:
?5874 ⊢ A0 : !?5880
subgoal 3 (ID 5877) is:
sub_in_env ?5874 N A0 0 (A0 :: Γ) Γ
subgoal 4 (ID 5878) is:
A0 :: Γ ⊣
subgoal 5 (ID 5857) is:
Γ ⊢ B [ ← N] : !t
subgoal 6 (ID 5752) is:
Γ ⊢ M' · N : B [ ← N]
subgoal 7 (ID 5753) is:
Γ ⊢ M · N' : B [ ← N]
subgoal 8 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using , ?5464 using , ?5470 using , ?5496 using , ?5502 using , ?5531 using , ?5532 using , ?5854 using ?5858 , ?5858 using , ?5865 using ?5872 , ?5866 using ?5874 , ?5867 using ?5875 , ?5872 using , ?5874 open, ?5875 using , ?5879 using , ?5880 open,)
apply H0. 7 subgoals, subgoal 1 (ID 5883)
Γ : Env
N : Term
A : Term
B : Term
H0 : Γ ⊢ N : A
IHtyp2 : forall N0 : Term, N → N0 -> Γ ⊢ N0 : A
A0 : Term
M0 : Term
IHtyp1 : forall N : Term, λ [A0], M0 → N -> Γ ⊢ N : Π (A), B
x : X.Sorts
s : X.Sorts
t : X.Sorts
u : X.Sorts
H1 : !x ≡ !u
H3 : Y.Rel s t u
H2 : Γ ⊢ A : !s
H5 : A :: Γ ⊢ B : !t
u1 : X.Sorts
u2 : X.Sorts
u3 : X.Sorts
D : Term
H4 : Y.Rel u1 u2 u3
H6 : Γ ⊢ A0 : !u1
H7 : A0 :: Γ ⊢ M0 : D
H8 : A0 :: Γ ⊢ D : !u2
H : A ≡ A0
H9 : B ≡ D
============================
Γ ⊢ A0 : !?5880
subgoal 2 (ID 5877) is:
sub_in_env Γ N A0 0 (A0 :: Γ) Γ
subgoal 3 (ID 5878) is:
A0 :: Γ ⊣
subgoal 4 (ID 5857) is:
Γ ⊢ B [ ← N] : !t
subgoal 5 (ID 5752) is:
Γ ⊢ M' · N : B [ ← N]
subgoal 6 (ID 5753) is:
Γ ⊢ M · N' : B [ ← N]
subgoal 7 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using , ?5464 using , ?5470 using , ?5496 using , ?5502 using , ?5531 using , ?5532 using , ?5854 using ?5858 , ?5858 using , ?5865 using ?5872 , ?5866 using ?5874 , ?5867 using ?5875 , ?5872 using , ?5874 using , ?5875 using , ?5879 using , ?5880 open,)
apply H6. 6 subgoals, subgoal 1 (ID 5877)
Γ : Env
N : Term
A : Term
B : Term
H0 : Γ ⊢ N : A
IHtyp2 : forall N0 : Term, N → N0 -> Γ ⊢ N0 : A
A0 : Term
M0 : Term
IHtyp1 : forall N : Term, λ [A0], M0 → N -> Γ ⊢ N : Π (A), B
x : X.Sorts
s : X.Sorts
t : X.Sorts
u : X.Sorts
H1 : !x ≡ !u
H3 : Y.Rel s t u
H2 : Γ ⊢ A : !s
H5 : A :: Γ ⊢ B : !t
u1 : X.Sorts
u2 : X.Sorts
u3 : X.Sorts
D : Term
H4 : Y.Rel u1 u2 u3
H6 : Γ ⊢ A0 : !u1
H7 : A0 :: Γ ⊢ M0 : D
H8 : A0 :: Γ ⊢ D : !u2
H : A ≡ A0
H9 : B ≡ D
============================
sub_in_env Γ N A0 0 (A0 :: Γ) Γ
subgoal 2 (ID 5878) is:
A0 :: Γ ⊣
subgoal 3 (ID 5857) is:
Γ ⊢ B [ ← N] : !t
subgoal 4 (ID 5752) is:
Γ ⊢ M' · N : B [ ← N]
subgoal 5 (ID 5753) is:
Γ ⊢ M · N' : B [ ← N]
subgoal 6 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using , ?5464 using , ?5470 using , ?5496 using , ?5502 using , ?5531 using , ?5532 using , ?5854 using ?5858 , ?5858 using , ?5865 using ?5872 , ?5866 using ?5874 , ?5867 using ?5875 , ?5872 using , ?5874 using , ?5875 using , ?5879 using , ?5880 using ,)
constructor.5 subgoals, subgoal 1 (ID 5878)
Γ : Env
N : Term
A : Term
B : Term
H0 : Γ ⊢ N : A
IHtyp2 : forall N0 : Term, N → N0 -> Γ ⊢ N0 : A
A0 : Term
M0 : Term
IHtyp1 : forall N : Term, λ [A0], M0 → N -> Γ ⊢ N : Π (A), B
x : X.Sorts
s : X.Sorts
t : X.Sorts
u : X.Sorts
H1 : !x ≡ !u
H3 : Y.Rel s t u
H2 : Γ ⊢ A : !s
H5 : A :: Γ ⊢ B : !t
u1 : X.Sorts
u2 : X.Sorts
u3 : X.Sorts
D : Term
H4 : Y.Rel u1 u2 u3
H6 : Γ ⊢ A0 : !u1
H7 : A0 :: Γ ⊢ M0 : D
H8 : A0 :: Γ ⊢ D : !u2
H : A ≡ A0
H9 : B ≡ D
============================
A0 :: Γ ⊣
subgoal 2 (ID 5857) is:
Γ ⊢ B [ ← N] : !t
subgoal 3 (ID 5752) is:
Γ ⊢ M' · N : B [ ← N]
subgoal 4 (ID 5753) is:
Γ ⊢ M · N' : B [ ← N]
subgoal 5 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using , ?5464 using , ?5470 using , ?5496 using , ?5502 using , ?5531 using , ?5532 using , ?5854 using ?5858 , ?5858 using , ?5865 using ?5872 , ?5866 using ?5874 , ?5867 using ?5875 , ?5872 using , ?5874 using , ?5875 using , ?5879 using , ?5880 using ,)
eauto. 4 subgoals, subgoal 1 (ID 5857)
Γ : Env
N : Term
A : Term
B : Term
H0 : Γ ⊢ N : A
IHtyp2 : forall N0 : Term, N → N0 -> Γ ⊢ N0 : A
A0 : Term
M0 : Term
IHtyp1 : forall N : Term, λ [A0], M0 → N -> Γ ⊢ N : Π (A), B
x : X.Sorts
s : X.Sorts
t : X.Sorts
u : X.Sorts
H1 : !x ≡ !u
H3 : Y.Rel s t u
H2 : Γ ⊢ A : !s
H5 : A :: Γ ⊢ B : !t
u1 : X.Sorts
u2 : X.Sorts
u3 : X.Sorts
D : Term
H4 : Y.Rel u1 u2 u3
H6 : Γ ⊢ A0 : !u1
H7 : A0 :: Γ ⊢ M0 : D
H8 : A0 :: Γ ⊢ D : !u2
H : A ≡ A0
H9 : B ≡ D
============================
Γ ⊢ B [ ← N] : !t
subgoal 2 (ID 5752) is:
Γ ⊢ M' · N : B [ ← N]
subgoal 3 (ID 5753) is:
Γ ⊢ M · N' : B [ ← N]
subgoal 4 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using , ?5464 using , ?5470 using , ?5496 using , ?5502 using , ?5531 using , ?5532 using , ?5854 using ?5858 , ?5858 using , ?5865 using ?5872 , ?5866 using ?5874 , ?5867 using ?5875 , ?5872 using , ?5874 using , ?5875 using , ?5879 using , ?5880 using , ?5885 using ,)
change !t with (!t [ ← N] ). 4 subgoals, subgoal 1 (ID 5896)
Γ : Env
N : Term
A : Term
B : Term
H0 : Γ ⊢ N : A
IHtyp2 : forall N0 : Term, N → N0 -> Γ ⊢ N0 : A
A0 : Term
M0 : Term
IHtyp1 : forall N : Term, λ [A0], M0 → N -> Γ ⊢ N : Π (A), B
x : X.Sorts
s : X.Sorts
t : X.Sorts
u : X.Sorts
H1 : !x ≡ !u
H3 : Y.Rel s t u
H2 : Γ ⊢ A : !s
H5 : A :: Γ ⊢ B : !t
u1 : X.Sorts
u2 : X.Sorts
u3 : X.Sorts
D : Term
H4 : Y.Rel u1 u2 u3
H6 : Γ ⊢ A0 : !u1
H7 : A0 :: Γ ⊢ M0 : D
H8 : A0 :: Γ ⊢ D : !u2
H : A ≡ A0
H9 : B ≡ D
============================
Γ ⊢ B [ ← N] : !t [ ← N]
subgoal 2 (ID 5752) is:
Γ ⊢ M' · N : B [ ← N]
subgoal 3 (ID 5753) is:
Γ ⊢ M · N' : B [ ← N]
subgoal 4 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using , ?5464 using , ?5470 using , ?5496 using , ?5502 using , ?5531 using , ?5532 using , ?5854 using ?5858 , ?5858 using , ?5865 using ?5872 , ?5866 using ?5874 , ?5867 using ?5875 , ?5872 using , ?5874 using , ?5875 using , ?5879 using , ?5880 using , ?5885 using ,)
eapply substitution. 7 subgoals, subgoal 1 (ID 5909)
Γ : Env
N : Term
A : Term
B : Term
H0 : Γ ⊢ N : A
IHtyp2 : forall N0 : Term, N → N0 -> Γ ⊢ N0 : A
A0 : Term
M0 : Term
IHtyp1 : forall N : Term, λ [A0], M0 → N -> Γ ⊢ N : Π (A), B
x : X.Sorts
s : X.Sorts
t : X.Sorts
u : X.Sorts
H1 : !x ≡ !u
H3 : Y.Rel s t u
H2 : Γ ⊢ A : !s
H5 : A :: Γ ⊢ B : !t
u1 : X.Sorts
u2 : X.Sorts
u3 : X.Sorts
D : Term
H4 : Y.Rel u1 u2 u3
H6 : Γ ⊢ A0 : !u1
H7 : A0 :: Γ ⊢ M0 : D
H8 : A0 :: Γ ⊢ D : !u2
H : A ≡ A0
H9 : B ≡ D
============================
?5908 ⊢ B : !t
subgoal 2 (ID 5912) is:
?5910 ⊢ N : ?5911
subgoal 3 (ID 5913) is:
sub_in_env ?5910 N ?5911 0 ?5908 Γ
subgoal 4 (ID 5914) is:
?5908 ⊣
subgoal 5 (ID 5752) is:
Γ ⊢ M' · N : B [ ← N]
subgoal 6 (ID 5753) is:
Γ ⊢ M · N' : B [ ← N]
subgoal 7 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using , ?5464 using , ?5470 using , ?5496 using , ?5502 using , ?5531 using , ?5532 using , ?5854 using ?5858 , ?5858 using , ?5865 using ?5872 , ?5866 using ?5874 , ?5867 using ?5875 , ?5872 using , ?5874 using , ?5875 using , ?5879 using , ?5880 using , ?5885 using , ?5901 using ?5908 , ?5902 using ?5910 , ?5903 using ?5911 , ?5908 open, ?5910 open, ?5911 open,)
apply H5. 6 subgoals, subgoal 1 (ID 5912)
Γ : Env
N : Term
A : Term
B : Term
H0 : Γ ⊢ N : A
IHtyp2 : forall N0 : Term, N → N0 -> Γ ⊢ N0 : A
A0 : Term
M0 : Term
IHtyp1 : forall N : Term, λ [A0], M0 → N -> Γ ⊢ N : Π (A), B
x : X.Sorts
s : X.Sorts
t : X.Sorts
u : X.Sorts
H1 : !x ≡ !u
H3 : Y.Rel s t u
H2 : Γ ⊢ A : !s
H5 : A :: Γ ⊢ B : !t
u1 : X.Sorts
u2 : X.Sorts
u3 : X.Sorts
D : Term
H4 : Y.Rel u1 u2 u3
H6 : Γ ⊢ A0 : !u1
H7 : A0 :: Γ ⊢ M0 : D
H8 : A0 :: Γ ⊢ D : !u2
H : A ≡ A0
H9 : B ≡ D
============================
?5910 ⊢ N : ?5911
subgoal 2 (ID 5913) is:
sub_in_env ?5910 N ?5911 0 (A :: Γ) Γ
subgoal 3 (ID 5914) is:
A :: Γ ⊣
subgoal 4 (ID 5752) is:
Γ ⊢ M' · N : B [ ← N]
subgoal 5 (ID 5753) is:
Γ ⊢ M · N' : B [ ← N]
subgoal 6 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using , ?5464 using , ?5470 using , ?5496 using , ?5502 using , ?5531 using , ?5532 using , ?5854 using ?5858 , ?5858 using , ?5865 using ?5872 , ?5866 using ?5874 , ?5867 using ?5875 , ?5872 using , ?5874 using , ?5875 using , ?5879 using , ?5880 using , ?5885 using , ?5901 using ?5908 , ?5902 using ?5910 , ?5903 using ?5911 , ?5908 using , ?5910 open, ?5911 open,)
apply H0. 5 subgoals, subgoal 1 (ID 5913)
Γ : Env
N : Term
A : Term
B : Term
H0 : Γ ⊢ N : A
IHtyp2 : forall N0 : Term, N → N0 -> Γ ⊢ N0 : A
A0 : Term
M0 : Term
IHtyp1 : forall N : Term, λ [A0], M0 → N -> Γ ⊢ N : Π (A), B
x : X.Sorts
s : X.Sorts
t : X.Sorts
u : X.Sorts
H1 : !x ≡ !u
H3 : Y.Rel s t u
H2 : Γ ⊢ A : !s
H5 : A :: Γ ⊢ B : !t
u1 : X.Sorts
u2 : X.Sorts
u3 : X.Sorts
D : Term
H4 : Y.Rel u1 u2 u3
H6 : Γ ⊢ A0 : !u1
H7 : A0 :: Γ ⊢ M0 : D
H8 : A0 :: Γ ⊢ D : !u2
H : A ≡ A0
H9 : B ≡ D
============================
sub_in_env Γ N A 0 (A :: Γ) Γ
subgoal 2 (ID 5914) is:
A :: Γ ⊣
subgoal 3 (ID 5752) is:
Γ ⊢ M' · N : B [ ← N]
subgoal 4 (ID 5753) is:
Γ ⊢ M · N' : B [ ← N]
subgoal 5 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using , ?5464 using , ?5470 using , ?5496 using , ?5502 using , ?5531 using , ?5532 using , ?5854 using ?5858 , ?5858 using , ?5865 using ?5872 , ?5866 using ?5874 , ?5867 using ?5875 , ?5872 using , ?5874 using , ?5875 using , ?5879 using , ?5880 using , ?5885 using , ?5901 using ?5908 , ?5902 using ?5910 , ?5903 using ?5911 , ?5908 using , ?5910 using , ?5911 using ,)
constructor.4 subgoals, subgoal 1 (ID 5914)
Γ : Env
N : Term
A : Term
B : Term
H0 : Γ ⊢ N : A
IHtyp2 : forall N0 : Term, N → N0 -> Γ ⊢ N0 : A
A0 : Term
M0 : Term
IHtyp1 : forall N : Term, λ [A0], M0 → N -> Γ ⊢ N : Π (A), B
x : X.Sorts
s : X.Sorts
t : X.Sorts
u : X.Sorts
H1 : !x ≡ !u
H3 : Y.Rel s t u
H2 : Γ ⊢ A : !s
H5 : A :: Γ ⊢ B : !t
u1 : X.Sorts
u2 : X.Sorts
u3 : X.Sorts
D : Term
H4 : Y.Rel u1 u2 u3
H6 : Γ ⊢ A0 : !u1
H7 : A0 :: Γ ⊢ M0 : D
H8 : A0 :: Γ ⊢ D : !u2
H : A ≡ A0
H9 : B ≡ D
============================
A :: Γ ⊣
subgoal 2 (ID 5752) is:
Γ ⊢ M' · N : B [ ← N]
subgoal 3 (ID 5753) is:
Γ ⊢ M · N' : B [ ← N]
subgoal 4 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using , ?5464 using , ?5470 using , ?5496 using , ?5502 using , ?5531 using , ?5532 using , ?5854 using ?5858 , ?5858 using , ?5865 using ?5872 , ?5866 using ?5874 , ?5867 using ?5875 , ?5872 using , ?5874 using , ?5875 using , ?5879 using , ?5880 using , ?5885 using , ?5901 using ?5908 , ?5902 using ?5910 , ?5903 using ?5911 , ?5908 using , ?5910 using , ?5911 using ,)
eauto.3 subgoals, subgoal 1 (ID 5752)
Γ : Env
M : Term
N : Term
A : Term
B : Term
H : Γ ⊢ M : Π (A), B
H0 : Γ ⊢ N : A
IHtyp1 : forall N : Term, M → N -> Γ ⊢ N : Π (A), B
IHtyp2 : forall N0 : Term, N → N0 -> Γ ⊢ N0 : A
M' : Term
H5 : M → M'
============================
Γ ⊢ M' · N : B [ ← N]
subgoal 2 (ID 5753) is:
Γ ⊢ M · N' : B [ ← N]
subgoal 3 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using , ?5464 using , ?5470 using , ?5496 using , ?5502 using , ?5531 using , ?5532 using , ?5854 using ?5858 , ?5858 using , ?5865 using ?5872 , ?5866 using ?5874 , ?5867 using ?5875 , ?5872 using , ?5874 using , ?5875 using , ?5879 using , ?5880 using , ?5885 using , ?5901 using ?5908 , ?5902 using ?5910 , ?5903 using ?5911 , ?5908 using , ?5910 using , ?5911 using , ?5916 using ,)
econstructor. 4 subgoals, subgoal 1 (ID 5932)
Γ : Env
M : Term
N : Term
A : Term
B : Term
H : Γ ⊢ M : Π (A), B
H0 : Γ ⊢ N : A
IHtyp1 : forall N : Term, M → N -> Γ ⊢ N : Π (A), B
IHtyp2 : forall N0 : Term, N → N0 -> Γ ⊢ N0 : A
M' : Term
H5 : M → M'
============================
Γ ⊢ M' : Π (?5931), B
subgoal 2 (ID 5933) is:
Γ ⊢ N : ?5931
subgoal 3 (ID 5753) is:
Γ ⊢ M · N' : B [ ← N]
subgoal 4 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using , ?5464 using , ?5470 using , ?5496 using , ?5502 using , ?5531 using , ?5532 using , ?5854 using ?5858 , ?5858 using , ?5865 using ?5872 , ?5866 using ?5874 , ?5867 using ?5875 , ?5872 using , ?5874 using , ?5875 using , ?5879 using , ?5880 using , ?5885 using , ?5901 using ?5908 , ?5902 using ?5910 , ?5903 using ?5911 , ?5908 using , ?5910 using , ?5911 using , ?5916 using , ?5931 open,)
eauto. 3 subgoals, subgoal 1 (ID 5933)
Γ : Env
M : Term
N : Term
A : Term
B : Term
H : Γ ⊢ M : Π (A), B
H0 : Γ ⊢ N : A
IHtyp1 : forall N : Term, M → N -> Γ ⊢ N : Π (A), B
IHtyp2 : forall N0 : Term, N → N0 -> Γ ⊢ N0 : A
M' : Term
H5 : M → M'
============================
Γ ⊢ N : A
subgoal 2 (ID 5753) is:
Γ ⊢ M · N' : B [ ← N]
subgoal 3 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using , ?5464 using , ?5470 using , ?5496 using , ?5502 using , ?5531 using , ?5532 using , ?5854 using ?5858 , ?5858 using , ?5865 using ?5872 , ?5866 using ?5874 , ?5867 using ?5875 , ?5872 using , ?5874 using , ?5875 using , ?5879 using , ?5880 using , ?5885 using , ?5901 using ?5908 , ?5902 using ?5910 , ?5903 using ?5911 , ?5908 using , ?5910 using , ?5911 using , ?5916 using , ?5931 using ,)
trivial.2 subgoals, subgoal 1 (ID 5753)
Γ : Env
M : Term
N : Term
A : Term
B : Term
H : Γ ⊢ M : Π (A), B
H0 : Γ ⊢ N : A
IHtyp1 : forall N : Term, M → N -> Γ ⊢ N : Π (A), B
IHtyp2 : forall N0 : Term, N → N0 -> Γ ⊢ N0 : A
N' : Term
H5 : N → N'
============================
Γ ⊢ M · N' : B [ ← N]
subgoal 2 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using , ?5464 using , ?5470 using , ?5496 using , ?5502 using , ?5531 using , ?5532 using , ?5854 using ?5858 , ?5858 using , ?5865 using ?5872 , ?5866 using ?5874 , ?5867 using ?5875 , ?5872 using , ?5874 using , ?5875 using , ?5879 using , ?5880 using , ?5885 using , ?5901 using ?5908 , ?5902 using ?5910 , ?5903 using ?5911 , ?5908 using , ?5910 using , ?5911 using , ?5916 using , ?5931 using ,)
assert (exists u, Γ ⊢ Π(A),B : !u). 3 subgoals, subgoal 1 (ID 5941)
Γ : Env
M : Term
N : Term
A : Term
B : Term
H : Γ ⊢ M : Π (A), B
H0 : Γ ⊢ N : A
IHtyp1 : forall N : Term, M → N -> Γ ⊢ N : Π (A), B
IHtyp2 : forall N0 : Term, N → N0 -> Γ ⊢ N0 : A
N' : Term
H5 : N → N'
============================
exists u : X.Sorts, Γ ⊢ Π (A), B : !u
subgoal 2 (ID 5942) is:
Γ ⊢ M · N' : B [ ← N]
subgoal 3 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using , ?5464 using , ?5470 using , ?5496 using , ?5502 using , ?5531 using , ?5532 using , ?5854 using ?5858 , ?5858 using , ?5865 using ?5872 , ?5866 using ?5874 , ?5867 using ?5875 , ?5872 using , ?5874 using , ?5875 using , ?5879 using , ?5880 using , ?5885 using , ?5901 using ?5908 , ?5902 using ?5910 , ?5903 using ?5911 , ?5908 using , ?5910 using , ?5911 using , ?5916 using , ?5931 using ,)
apply TypeCorrect in H.3 subgoals, subgoal 1 (ID 5944)
Γ : Env
M : Term
N : Term
A : Term
B : Term
H : (exists s : X.Sorts, Π (A), B = !s) \/
(exists s : X.Sorts, Γ ⊢ Π (A), B : !s)
H0 : Γ ⊢ N : A
IHtyp1 : forall N : Term, M → N -> Γ ⊢ N : Π (A), B
IHtyp2 : forall N0 : Term, N → N0 -> Γ ⊢ N0 : A
N' : Term
H5 : N → N'
============================
exists u : X.Sorts, Γ ⊢ Π (A), B : !u
subgoal 2 (ID 5942) is:
Γ ⊢ M · N' : B [ ← N]
subgoal 3 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using , ?5464 using , ?5470 using , ?5496 using , ?5502 using , ?5531 using , ?5532 using , ?5854 using ?5858 , ?5858 using , ?5865 using ?5872 , ?5866 using ?5874 , ?5867 using ?5875 , ?5872 using , ?5874 using , ?5875 using , ?5879 using , ?5880 using , ?5885 using , ?5901 using ?5908 , ?5902 using ?5910 , ?5903 using ?5911 , ?5908 using , ?5910 using , ?5911 using , ?5916 using , ?5931 using ,)
destruct H. 4 subgoals, subgoal 1 (ID 5950)
Γ : Env
M : Term
N : Term
A : Term
B : Term
H : exists s : X.Sorts, Π (A), B = !s
H0 : Γ ⊢ N : A
IHtyp1 : forall N : Term, M → N -> Γ ⊢ N : Π (A), B
IHtyp2 : forall N0 : Term, N → N0 -> Γ ⊢ N0 : A
N' : Term
H5 : N → N'
============================
exists u : X.Sorts, Γ ⊢ Π (A), B : !u
subgoal 2 (ID 5952) is:
exists u : X.Sorts, Γ ⊢ Π (A), B : !u
subgoal 3 (ID 5942) is:
Γ ⊢ M · N' : B [ ← N]
subgoal 4 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using , ?5464 using , ?5470 using , ?5496 using , ?5502 using , ?5531 using , ?5532 using , ?5854 using ?5858 , ?5858 using , ?5865 using ?5872 , ?5866 using ?5874 , ?5867 using ?5875 , ?5872 using , ?5874 using , ?5875 using , ?5879 using , ?5880 using , ?5885 using , ?5901 using ?5908 , ?5902 using ?5910 , ?5903 using ?5911 , ?5908 using , ?5910 using , ?5911 using , ?5916 using , ?5931 using ,)
destruct H; discriminate. 3 subgoals, subgoal 1 (ID 5952)
Γ : Env
M : Term
N : Term
A : Term
B : Term
H : exists s : X.Sorts, Γ ⊢ Π (A), B : !s
H0 : Γ ⊢ N : A
IHtyp1 : forall N : Term, M → N -> Γ ⊢ N : Π (A), B
IHtyp2 : forall N0 : Term, N → N0 -> Γ ⊢ N0 : A
N' : Term
H5 : N → N'
============================
exists u : X.Sorts, Γ ⊢ Π (A), B : !u
subgoal 2 (ID 5942) is:
Γ ⊢ M · N' : B [ ← N]
subgoal 3 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using , ?5464 using , ?5470 using , ?5496 using , ?5502 using , ?5531 using , ?5532 using , ?5854 using ?5858 , ?5858 using , ?5865 using ?5872 , ?5866 using ?5874 , ?5867 using ?5875 , ?5872 using , ?5874 using , ?5875 using , ?5879 using , ?5880 using , ?5885 using , ?5901 using ?5908 , ?5902 using ?5910 , ?5903 using ?5911 , ?5908 using , ?5910 using , ?5911 using , ?5916 using , ?5931 using ,)
trivial.2 subgoals, subgoal 1 (ID 5942)
Γ : Env
M : Term
N : Term
A : Term
B : Term
H : Γ ⊢ M : Π (A), B
H0 : Γ ⊢ N : A
IHtyp1 : forall N : Term, M → N -> Γ ⊢ N : Π (A), B
IHtyp2 : forall N0 : Term, N → N0 -> Γ ⊢ N0 : A
N' : Term
H5 : N → N'
H1 : exists u : X.Sorts, Γ ⊢ Π (A), B : !u
============================
Γ ⊢ M · N' : B [ ← N]
subgoal 2 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using , ?5464 using , ?5470 using , ?5496 using , ?5502 using , ?5531 using , ?5532 using , ?5854 using ?5858 , ?5858 using , ?5865 using ?5872 , ?5866 using ?5874 , ?5867 using ?5875 , ?5872 using , ?5874 using , ?5875 using , ?5879 using , ?5880 using , ?5885 using , ?5901 using ?5908 , ?5902 using ?5910 , ?5903 using ?5911 , ?5908 using , ?5910 using , ?5911 using , ?5916 using , ?5931 using ,)
destruct H1. 2 subgoals, subgoal 1 (ID 5967)
Γ : Env
M : Term
N : Term
A : Term
B : Term
H : Γ ⊢ M : Π (A), B
H0 : Γ ⊢ N : A
IHtyp1 : forall N : Term, M → N -> Γ ⊢ N : Π (A), B
IHtyp2 : forall N0 : Term, N → N0 -> Γ ⊢ N0 : A
N' : Term
H5 : N → N'
x : X.Sorts
H1 : Γ ⊢ Π (A), B : !x
============================
Γ ⊢ M · N' : B [ ← N]
subgoal 2 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using , ?5464 using , ?5470 using , ?5496 using , ?5502 using , ?5531 using , ?5532 using , ?5854 using ?5858 , ?5858 using , ?5865 using ?5872 , ?5866 using ?5874 , ?5867 using ?5875 , ?5872 using , ?5874 using , ?5875 using , ?5879 using , ?5880 using , ?5885 using , ?5901 using ?5908 , ?5902 using ?5910 , ?5903 using ?5911 , ?5908 using , ?5910 using , ?5911 using , ?5916 using , ?5931 using ,)
apply gen_pi in H1 as (s & t & u & h); decompose [and] h; clear h.2 subgoals, subgoal 1 (ID 5999)
Γ : Env
M : Term
N : Term
A : Term
B : Term
H : Γ ⊢ M : Π (A), B
H0 : Γ ⊢ N : A
IHtyp1 : forall N : Term, M → N -> Γ ⊢ N : Π (A), B
IHtyp2 : forall N0 : Term, N → N0 -> Γ ⊢ N0 : A
N' : Term
H5 : N → N'
x : X.Sorts
s : X.Sorts
t : X.Sorts
u : X.Sorts
H1 : !x ≡ !u
H3 : Y.Rel s t u
H2 : Γ ⊢ A : !s
H6 : A :: Γ ⊢ B : !t
============================
Γ ⊢ M · N' : B [ ← N]
subgoal 2 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using , ?5464 using , ?5470 using , ?5496 using , ?5502 using , ?5531 using , ?5532 using , ?5854 using ?5858 , ?5858 using , ?5865 using ?5872 , ?5866 using ?5874 , ?5867 using ?5875 , ?5872 using , ?5874 using , ?5875 using , ?5879 using , ?5880 using , ?5885 using , ?5901 using ?5908 , ?5902 using ?5910 , ?5903 using ?5911 , ?5908 using , ?5910 using , ?5911 using , ?5916 using , ?5931 using ,)
apply Cnv with (B [← N']) t. 4 subgoals, subgoal 1 (ID 6000)
Γ : Env
M : Term
N : Term
A : Term
B : Term
H : Γ ⊢ M : Π (A), B
H0 : Γ ⊢ N : A
IHtyp1 : forall N : Term, M → N -> Γ ⊢ N : Π (A), B
IHtyp2 : forall N0 : Term, N → N0 -> Γ ⊢ N0 : A
N' : Term
H5 : N → N'
x : X.Sorts
s : X.Sorts
t : X.Sorts
u : X.Sorts
H1 : !x ≡ !u
H3 : Y.Rel s t u
H2 : Γ ⊢ A : !s
H6 : A :: Γ ⊢ B : !t
============================
B [ ← N'] ≡ B [ ← N]
subgoal 2 (ID 6001) is:
Γ ⊢ M · N' : B [ ← N']
subgoal 3 (ID 6002) is:
Γ ⊢ B [ ← N] : !t
subgoal 4 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using , ?5464 using , ?5470 using , ?5496 using , ?5502 using , ?5531 using , ?5532 using , ?5854 using ?5858 , ?5858 using , ?5865 using ?5872 , ?5866 using ?5874 , ?5867 using ?5875 , ?5872 using , ?5874 using , ?5875 using , ?5879 using , ?5880 using , ?5885 using , ?5901 using ?5908 , ?5902 using ?5910 , ?5903 using ?5911 , ?5908 using , ?5910 using , ?5911 using , ?5916 using , ?5931 using ,)
apply Betac_subst. 4 subgoals, subgoal 1 (ID 6003)
Γ : Env
M : Term
N : Term
A : Term
B : Term
H : Γ ⊢ M : Π (A), B
H0 : Γ ⊢ N : A
IHtyp1 : forall N : Term, M → N -> Γ ⊢ N : Π (A), B
IHtyp2 : forall N0 : Term, N → N0 -> Γ ⊢ N0 : A
N' : Term
H5 : N → N'
x : X.Sorts
s : X.Sorts
t : X.Sorts
u : X.Sorts
H1 : !x ≡ !u
H3 : Y.Rel s t u
H2 : Γ ⊢ A : !s
H6 : A :: Γ ⊢ B : !t
============================
N' ≡ N
subgoal 2 (ID 6001) is:
Γ ⊢ M · N' : B [ ← N']
subgoal 3 (ID 6002) is:
Γ ⊢ B [ ← N] : !t
subgoal 4 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using , ?5464 using , ?5470 using , ?5496 using , ?5502 using , ?5531 using , ?5532 using , ?5854 using ?5858 , ?5858 using , ?5865 using ?5872 , ?5866 using ?5874 , ?5867 using ?5875 , ?5872 using , ?5874 using , ?5875 using , ?5879 using , ?5880 using , ?5885 using , ?5901 using ?5908 , ?5902 using ?5910 , ?5903 using ?5911 , ?5908 using , ?5910 using , ?5911 using , ?5916 using , ?5931 using ,)
auto.3 subgoals, subgoal 1 (ID 6001)
Γ : Env
M : Term
N : Term
A : Term
B : Term
H : Γ ⊢ M : Π (A), B
H0 : Γ ⊢ N : A
IHtyp1 : forall N : Term, M → N -> Γ ⊢ N : Π (A), B
IHtyp2 : forall N0 : Term, N → N0 -> Γ ⊢ N0 : A
N' : Term
H5 : N → N'
x : X.Sorts
s : X.Sorts
t : X.Sorts
u : X.Sorts
H1 : !x ≡ !u
H3 : Y.Rel s t u
H2 : Γ ⊢ A : !s
H6 : A :: Γ ⊢ B : !t
============================
Γ ⊢ M · N' : B [ ← N']
subgoal 2 (ID 6002) is:
Γ ⊢ B [ ← N] : !t
subgoal 3 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using , ?5464 using , ?5470 using , ?5496 using , ?5502 using , ?5531 using , ?5532 using , ?5854 using ?5858 , ?5858 using , ?5865 using ?5872 , ?5866 using ?5874 , ?5867 using ?5875 , ?5872 using , ?5874 using , ?5875 using , ?5879 using , ?5880 using , ?5885 using , ?5901 using ?5908 , ?5902 using ?5910 , ?5903 using ?5911 , ?5908 using , ?5910 using , ?5911 using , ?5916 using , ?5931 using ,)
econstructor. 4 subgoals, subgoal 1 (ID 6022)
Γ : Env
M : Term
N : Term
A : Term
B : Term
H : Γ ⊢ M : Π (A), B
H0 : Γ ⊢ N : A
IHtyp1 : forall N : Term, M → N -> Γ ⊢ N : Π (A), B
IHtyp2 : forall N0 : Term, N → N0 -> Γ ⊢ N0 : A
N' : Term
H5 : N → N'
x : X.Sorts
s : X.Sorts
t : X.Sorts
u : X.Sorts
H1 : !x ≡ !u
H3 : Y.Rel s t u
H2 : Γ ⊢ A : !s
H6 : A :: Γ ⊢ B : !t
============================
Γ ⊢ M : Π (?6021), B
subgoal 2 (ID 6023) is:
Γ ⊢ N' : ?6021
subgoal 3 (ID 6002) is:
Γ ⊢ B [ ← N] : !t
subgoal 4 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using , ?5464 using , ?5470 using , ?5496 using , ?5502 using , ?5531 using , ?5532 using , ?5854 using ?5858 , ?5858 using , ?5865 using ?5872 , ?5866 using ?5874 , ?5867 using ?5875 , ?5872 using , ?5874 using , ?5875 using , ?5879 using , ?5880 using , ?5885 using , ?5901 using ?5908 , ?5902 using ?5910 , ?5903 using ?5911 , ?5908 using , ?5910 using , ?5911 using , ?5916 using , ?5931 using , ?6021 open,)
apply H. 3 subgoals, subgoal 1 (ID 6023)
Γ : Env
M : Term
N : Term
A : Term
B : Term
H : Γ ⊢ M : Π (A), B
H0 : Γ ⊢ N : A
IHtyp1 : forall N : Term, M → N -> Γ ⊢ N : Π (A), B
IHtyp2 : forall N0 : Term, N → N0 -> Γ ⊢ N0 : A
N' : Term
H5 : N → N'
x : X.Sorts
s : X.Sorts
t : X.Sorts
u : X.Sorts
H1 : !x ≡ !u
H3 : Y.Rel s t u
H2 : Γ ⊢ A : !s
H6 : A :: Γ ⊢ B : !t
============================
Γ ⊢ N' : A
subgoal 2 (ID 6002) is:
Γ ⊢ B [ ← N] : !t
subgoal 3 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using , ?5464 using , ?5470 using , ?5496 using , ?5502 using , ?5531 using , ?5532 using , ?5854 using ?5858 , ?5858 using , ?5865 using ?5872 , ?5866 using ?5874 , ?5867 using ?5875 , ?5872 using , ?5874 using , ?5875 using , ?5879 using , ?5880 using , ?5885 using , ?5901 using ?5908 , ?5902 using ?5910 , ?5903 using ?5911 , ?5908 using , ?5910 using , ?5911 using , ?5916 using , ?5931 using , ?6021 using ,)
eauto.2 subgoals, subgoal 1 (ID 6002)
Γ : Env
M : Term
N : Term
A : Term
B : Term
H : Γ ⊢ M : Π (A), B
H0 : Γ ⊢ N : A
IHtyp1 : forall N : Term, M → N -> Γ ⊢ N : Π (A), B
IHtyp2 : forall N0 : Term, N → N0 -> Γ ⊢ N0 : A
N' : Term
H5 : N → N'
x : X.Sorts
s : X.Sorts
t : X.Sorts
u : X.Sorts
H1 : !x ≡ !u
H3 : Y.Rel s t u
H2 : Γ ⊢ A : !s
H6 : A :: Γ ⊢ B : !t
============================
Γ ⊢ B [ ← N] : !t
subgoal 2 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using , ?5464 using , ?5470 using , ?5496 using , ?5502 using , ?5531 using , ?5532 using , ?5854 using ?5858 , ?5858 using , ?5865 using ?5872 , ?5866 using ?5874 , ?5867 using ?5875 , ?5872 using , ?5874 using , ?5875 using , ?5879 using , ?5880 using , ?5885 using , ?5901 using ?5908 , ?5902 using ?5910 , ?5903 using ?5911 , ?5908 using , ?5910 using , ?5911 using , ?5916 using , ?5931 using , ?6021 using ,)
change !t with (!t [ ← N] ). 2 subgoals, subgoal 1 (ID 6031)
Γ : Env
M : Term
N : Term
A : Term
B : Term
H : Γ ⊢ M : Π (A), B
H0 : Γ ⊢ N : A
IHtyp1 : forall N : Term, M → N -> Γ ⊢ N : Π (A), B
IHtyp2 : forall N0 : Term, N → N0 -> Γ ⊢ N0 : A
N' : Term
H5 : N → N'
x : X.Sorts
s : X.Sorts
t : X.Sorts
u : X.Sorts
H1 : !x ≡ !u
H3 : Y.Rel s t u
H2 : Γ ⊢ A : !s
H6 : A :: Γ ⊢ B : !t
============================
Γ ⊢ B [ ← N] : !t [ ← N]
subgoal 2 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using , ?5464 using , ?5470 using , ?5496 using , ?5502 using , ?5531 using , ?5532 using , ?5854 using ?5858 , ?5858 using , ?5865 using ?5872 , ?5866 using ?5874 , ?5867 using ?5875 , ?5872 using , ?5874 using , ?5875 using , ?5879 using , ?5880 using , ?5885 using , ?5901 using ?5908 , ?5902 using ?5910 , ?5903 using ?5911 , ?5908 using , ?5910 using , ?5911 using , ?5916 using , ?5931 using , ?6021 using ,)
eapply substitution. 5 subgoals, subgoal 1 (ID 6044)
Γ : Env
M : Term
N : Term
A : Term
B : Term
H : Γ ⊢ M : Π (A), B
H0 : Γ ⊢ N : A
IHtyp1 : forall N : Term, M → N -> Γ ⊢ N : Π (A), B
IHtyp2 : forall N0 : Term, N → N0 -> Γ ⊢ N0 : A
N' : Term
H5 : N → N'
x : X.Sorts
s : X.Sorts
t : X.Sorts
u : X.Sorts
H1 : !x ≡ !u
H3 : Y.Rel s t u
H2 : Γ ⊢ A : !s
H6 : A :: Γ ⊢ B : !t
============================
?6043 ⊢ B : !t
subgoal 2 (ID 6047) is:
?6045 ⊢ N : ?6046
subgoal 3 (ID 6048) is:
sub_in_env ?6045 N ?6046 0 ?6043 Γ
subgoal 4 (ID 6049) is:
?6043 ⊣
subgoal 5 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using , ?5464 using , ?5470 using , ?5496 using , ?5502 using , ?5531 using , ?5532 using , ?5854 using ?5858 , ?5858 using , ?5865 using ?5872 , ?5866 using ?5874 , ?5867 using ?5875 , ?5872 using , ?5874 using , ?5875 using , ?5879 using , ?5880 using , ?5885 using , ?5901 using ?5908 , ?5902 using ?5910 , ?5903 using ?5911 , ?5908 using , ?5910 using , ?5911 using , ?5916 using , ?5931 using , ?6021 using , ?6036 using ?6043 , ?6037 using ?6045 , ?6038 using ?6046 , ?6043 open, ?6045 open, ?6046 open,)
apply H6. 4 subgoals, subgoal 1 (ID 6047)
Γ : Env
M : Term
N : Term
A : Term
B : Term
H : Γ ⊢ M : Π (A), B
H0 : Γ ⊢ N : A
IHtyp1 : forall N : Term, M → N -> Γ ⊢ N : Π (A), B
IHtyp2 : forall N0 : Term, N → N0 -> Γ ⊢ N0 : A
N' : Term
H5 : N → N'
x : X.Sorts
s : X.Sorts
t : X.Sorts
u : X.Sorts
H1 : !x ≡ !u
H3 : Y.Rel s t u
H2 : Γ ⊢ A : !s
H6 : A :: Γ ⊢ B : !t
============================
?6045 ⊢ N : ?6046
subgoal 2 (ID 6048) is:
sub_in_env ?6045 N ?6046 0 (A :: Γ) Γ
subgoal 3 (ID 6049) is:
A :: Γ ⊣
subgoal 4 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using , ?5464 using , ?5470 using , ?5496 using , ?5502 using , ?5531 using , ?5532 using , ?5854 using ?5858 , ?5858 using , ?5865 using ?5872 , ?5866 using ?5874 , ?5867 using ?5875 , ?5872 using , ?5874 using , ?5875 using , ?5879 using , ?5880 using , ?5885 using , ?5901 using ?5908 , ?5902 using ?5910 , ?5903 using ?5911 , ?5908 using , ?5910 using , ?5911 using , ?5916 using , ?5931 using , ?6021 using , ?6036 using ?6043 , ?6037 using ?6045 , ?6038 using ?6046 , ?6043 using , ?6045 open, ?6046 open,)
apply H0. 3 subgoals, subgoal 1 (ID 6048)
Γ : Env
M : Term
N : Term
A : Term
B : Term
H : Γ ⊢ M : Π (A), B
H0 : Γ ⊢ N : A
IHtyp1 : forall N : Term, M → N -> Γ ⊢ N : Π (A), B
IHtyp2 : forall N0 : Term, N → N0 -> Γ ⊢ N0 : A
N' : Term
H5 : N → N'
x : X.Sorts
s : X.Sorts
t : X.Sorts
u : X.Sorts
H1 : !x ≡ !u
H3 : Y.Rel s t u
H2 : Γ ⊢ A : !s
H6 : A :: Γ ⊢ B : !t
============================
sub_in_env Γ N A 0 (A :: Γ) Γ
subgoal 2 (ID 6049) is:
A :: Γ ⊣
subgoal 3 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using , ?5464 using , ?5470 using , ?5496 using , ?5502 using , ?5531 using , ?5532 using , ?5854 using ?5858 , ?5858 using , ?5865 using ?5872 , ?5866 using ?5874 , ?5867 using ?5875 , ?5872 using , ?5874 using , ?5875 using , ?5879 using , ?5880 using , ?5885 using , ?5901 using ?5908 , ?5902 using ?5910 , ?5903 using ?5911 , ?5908 using , ?5910 using , ?5911 using , ?5916 using , ?5931 using , ?6021 using , ?6036 using ?6043 , ?6037 using ?6045 , ?6038 using ?6046 , ?6043 using , ?6045 using , ?6046 using ,)
constructor.2 subgoals, subgoal 1 (ID 6049)
Γ : Env
M : Term
N : Term
A : Term
B : Term
H : Γ ⊢ M : Π (A), B
H0 : Γ ⊢ N : A
IHtyp1 : forall N : Term, M → N -> Γ ⊢ N : Π (A), B
IHtyp2 : forall N0 : Term, N → N0 -> Γ ⊢ N0 : A
N' : Term
H5 : N → N'
x : X.Sorts
s : X.Sorts
t : X.Sorts
u : X.Sorts
H1 : !x ≡ !u
H3 : Y.Rel s t u
H2 : Γ ⊢ A : !s
H6 : A :: Γ ⊢ B : !t
============================
A :: Γ ⊣
subgoal 2 (ID 2677) is:
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using , ?5464 using , ?5470 using , ?5496 using , ?5502 using , ?5531 using , ?5532 using , ?5854 using ?5858 , ?5858 using , ?5865 using ?5872 , ?5866 using ?5874 , ?5867 using ?5875 , ?5872 using , ?5874 using , ?5875 using , ?5879 using , ?5880 using , ?5885 using , ?5901 using ?5908 , ?5902 using ?5910 , ?5903 using ?5911 , ?5908 using , ?5910 using , ?5911 using , ?5916 using , ?5931 using , ?6021 using , ?6036 using ?6043 , ?6037 using ?6045 , ?6038 using ?6046 , ?6043 using , ?6045 using , ?6046 using ,)
eauto.1 subgoals, subgoal 1 (ID 2677)
Γ : Env
M : Term
A : Term
B : Term
s : X.Sorts
H : A ≡ B
H0 : Γ ⊢ M : A
H1 : Γ ⊢ B : !s
IHtyp1 : forall N : Term, M → N -> Γ ⊢ N : A
IHtyp2 : forall N : Term, B → N -> Γ ⊢ N : !s
N : Term
H2 : M → N
============================
Γ ⊢ N : B
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using , ?5464 using , ?5470 using , ?5496 using , ?5502 using , ?5531 using , ?5532 using , ?5854 using ?5858 , ?5858 using , ?5865 using ?5872 , ?5866 using ?5874 , ?5867 using ?5875 , ?5872 using , ?5874 using , ?5875 using , ?5879 using , ?5880 using , ?5885 using , ?5901 using ?5908 , ?5902 using ?5910 , ?5903 using ?5911 , ?5908 using , ?5910 using , ?5911 using , ?5916 using , ?5931 using , ?6021 using , ?6036 using ?6043 , ?6037 using ?6045 , ?6038 using ?6046 , ?6043 using , ?6045 using , ?6046 using , ?6051 using ,)
eauto.No more subgoals.
(dependent evars: ?3103 using , ?3104 using , ?3123 using , ?3124 using , ?3143 using , ?3147 using , ?3351 using , ?3352 using , ?3377 using , ?3378 using , ?3379 using , ?5170 using , ?5171 using , ?5451 using , ?5452 using , ?5453 using , ?5464 using , ?5470 using , ?5496 using , ?5502 using , ?5531 using , ?5532 using , ?5854 using ?5858 , ?5858 using , ?5865 using ?5872 , ?5866 using ?5874 , ?5867 using ?5875 , ?5872 using , ?5874 using , ?5875 using , ?5879 using , ?5880 using , ?5885 using , ?5901 using ?5908 , ?5902 using ?5910 , ?5903 using ?5911 , ?5908 using , ?5910 using , ?5911 using , ?5916 using , ?5931 using , ?6021 using , ?6036 using ?6043 , ?6037 using ?6045 , ?6038 using ?6046 , ?6043 using , ?6045 using , ?6046 using , ?6051 using , ?6061 using , ?6062 using ,)
Qed.
With both lemmas, we can now prove the full SR.
Reduction in the type is valid.
Wellformation of a context after reduction.
In its complete form: SubjectReduction.