Built with Alectryon, running Coq+SerAPI v8.17.0+0.17.1. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+βCtrl+β to navigate, Ctrl+π±οΈ to focus. On Mac, use β instead of Ctrl.
Notation"`0" := (Zer) : ty_scope.Notation"`1" := (One) : ty_scope.Notation"A `Γ B" := (Prod A B) (at level40) : ty_scope.Notation"A `+ B" := (Sum A B) (at level40) : ty_scope.Notation"A `β B" := (Arr A B) (at level40) : ty_scope .Variantty : Type :=
| LTy : pre_ty -> ty
| RTy : pre_ty -> ty
.DeriveNoConfusionfor ty.Bind Scope ty_scope with ty.#[global] CoercionLTy : pre_ty >-> ty.#[global] Notation"β t" := (LTy t) (at level5) : ty_scope .#[global] Notation"Β¬ t" := (RTy t) (at level5) : ty_scope .Open Scope ty_scope.Equationst_neg : ty -> ty :=
t_neg βa := Β¬a ;
t_neg Β¬a := βa .Notation"a β " := (t_neg a) (at level5) : ty_scope.Definitiont_ctx : Type := ctx ty.Bind Scope ctx_scope with t_ctx.Inductiveterm : t_ctx -> ty -> Type :=
| Val {Ξ A} : whn Ξ A -> term Ξ βA
| Mu {Ξ A} : state (Ξ βΆβ Β¬A) -> term Ξ βA
| VarR {Ξ A} : Ξ β Β¬A -> term Ξ Β¬A
| MuT {Ξ A} : state (Ξ βΆβ βA) -> term Ξ Β¬A
| Boom {Ξ} : term Ξ Β¬`0
| Case {Ξ A B} : state (Ξ βΆβ βA) -> state (Ξ βΆβ βB) -> term Ξ Β¬(A `+ B)
| Fst {Ξ A B} : term Ξ Β¬A -> term Ξ Β¬(A `Γ B)
| Snd {Ξ A B} : term Ξ Β¬B -> term Ξ Β¬(A `Γ B)
| App {Ξ A B} : whn Ξ A -> term Ξ Β¬B -> term Ξ Β¬(A `β B)
with whn : t_ctx -> pre_ty -> Type :=
| VarL {Ξ A} : Ξ β βA -> whn Ξ A
| Inl {Ξ A B} : whn Ξ A -> whn Ξ (A `+ B)
| Inr {Ξ A B} : whn Ξ B -> whn Ξ (A `+ B)
| Tt {Ξ} : whn Ξ `1
| Pair {Ξ A B} : state (Ξ βΆβ Β¬A) -> state (Ξ βΆβ Β¬B) -> whn Ξ (A `Γ B)
| Lam {Ξ A B} : state (Ξ βΆβ β(A `β B) βΆβ βA βΆβ Β¬B) -> whn Ξ (A `β B)
with state : t_ctx -> Type :=
| Cut {Ξ A} : term Ξ βA -> term Ξ Β¬A -> state Ξ
.DefinitionCut' {ΞA} : term Ξ A -> term Ξ Aβ -> state Ξ
:= match A with
| β_ => funxy => Cut x y
| Β¬_ => funxy => Cut y x
end .Equationsval : t_ctx -> ty -> Type :=
val Ξ βA := whn Ξ A ;
val Ξ Β¬A := term Ξ Β¬A .EquationsVarΞA : Ξ β A -> val Ξ A :=
Var _ β_ i := VarL i ;
Var _ Β¬_ i := VarR i .Arguments Var {Ξ} [A] i.Equationst_of_vΞA : val Ξ A -> term Ξ A :=
t_of_v _ β_ v := Val v ;
t_of_v _ Β¬_ k := k .Arguments t_of_v [Ξ A] v.Coerciont_of_v : val >-> term.Equationst_rename : term ββ β¦ c_var , term β§β :=
t_rename _ _ (Mu c) _ f := Mu (s_rename _ c _ (r_shift1 f)) ;
t_rename _ _ (Val v) _ f := Val (w_rename _ _ v _ f) ;
t_rename _ _ (VarR i) _ f := VarR (f _ i) ;
t_rename _ _ (MuT c) _ f := MuT (s_rename _ c _ (r_shift1 f)) ;
t_rename _ _ (Boom) _ f := Boom ;
t_rename _ _ (App u k) _ f := App (w_rename _ _ u _ f) (t_rename _ _ k _ f) ;
t_rename _ _ (Fst k) _ f := Fst (t_rename _ _ k _ f) ;
t_rename _ _ (Snd k) _ f := Snd (t_rename _ _ k _ f) ;
t_rename _ _ (Case u v) _ f :=
Case (s_rename _ u _ (r_shift1 f))
(s_rename _ v _ (r_shift1 f))
with w_rename : whn ββ β¦ c_var , val β§β :=
w_rename _ _ (VarL i) _ f := VarL (f _ i) ;
w_rename _ _ (Tt) _ f := Tt ;
w_rename _ _ (Lam u) _ f := Lam (s_rename _ u _ (r_shift3 f)) ;
w_rename _ _ (Pair u v) _ f :=
Pair (s_rename _ u _ (r_shift1 f))
(s_rename _ v _ (r_shift1 f)) ;
w_rename _ _ (Inl u) _ f := Inl (w_rename _ _ u _ f) ;
w_rename _ _ (Inr u) _ f := Inr (w_rename _ _ u _ f)
with s_rename : state ββ β¦ c_var , state β§β :=
s_rename _ (Cut v k) _ f := Cut (t_rename _ _ v _ f) (t_rename _ _ k _ f) .Equationsv_rename : val ββ β¦ c_var , val β§β :=
v_rename _ β_ v _ f := w_rename _ _ v _ f ;
v_rename _ Β¬_ k _ f := t_rename _ _ k _ f .Notation"t ββα΅£ r" := (t_rename _ _ t _ r%asgn) (at level14).Notation"w `α΅₯βα΅£ r" := (w_rename _ _ w _ r%asgn) (at level14).Notation"v α΅₯βα΅£ r" := (v_rename _ _ v _ r%asgn) (at level14).Notation"s ββα΅£ r" := (s_rename _ s _ r%asgn) (at level14).Definitiona_ren {Ξ1Ξ2Ξ3} : Ξ1 =[val]> Ξ2 -> Ξ2 β Ξ3 -> Ξ1 =[val]> Ξ3 :=
funfg_i => v_rename _ _ (f _ i) _ g .Arguments a_ren {_ _ _} _ _ _ _ /.Notation"a βα΅£ r" := (a_ren a r%asgn) (at level14) : asgn_scope.Definitiont_shift1 {ΞA} : term Ξ βα΅’ term (Ξ βΆβ A) := fun_t => t ββα΅£ r_pop.Definitionw_shift1 {ΞA} : whn Ξ βα΅’ whn (Ξ βΆβ A) := fun_w => w `α΅₯βα΅£ r_pop.Definitions_shift1 {ΞA} : state Ξ -> state (Ξ βΆβ A) := funs => s ββα΅£ r_pop.Definitionv_shift1 {ΞA} : val Ξ βα΅’ val (Ξ βΆβ A) := fun_v => v α΅₯βα΅£ r_pop.Definitionv_shift3 {ΞABC} : val Ξ βα΅’ val (Ξ βΆβ A βΆβ B βΆβ C)
:= fun_v => v α΅₯βα΅£ (r_pop α΅£β r_pop α΅£β r_pop).Definitiona_shift1 {ΞΞ} [A] (a : Ξ =[val]> Ξ) : (Ξ βΆβ A) =[val]> (Ξ βΆβ A)
:= [ fun_i => v_shift1 _ (a _ i) ,β Var top ].Definitiona_shift3 {ΞΞ} [A B C] (a : Ξ =[val]> Ξ)
: (Ξ βΆβ A βΆβ B βΆβ C) =[val]> (Ξ βΆβ A βΆβ B βΆβ C)
:= [ [ [ fun_i => v_shift3 _ (a _ i) ,β
Var (pop (pop top)) ] ,β
Var (pop top) ] ,β
Var top ].Equationst_subst : term ββ β¦ val , term β§β :=
t_subst _ _ (Mu c) _ f := Mu (s_subst _ c _ (a_shift1 f)) ;
t_subst _ _ (Val v) _ f := Val (w_subst _ _ v _ f) ;
t_subst _ _ (VarR i) _ f := f _ i ;
t_subst _ _ (MuT c) _ f := MuT (s_subst _ c _ (a_shift1 f)) ;
t_subst _ _ (Boom) _ f := Boom ;
t_subst _ _ (App u k) _ f := App (w_subst _ _ u _ f) (t_subst _ _ k _ f) ;
t_subst _ _ (Fst k) _ f := Fst (t_subst _ _ k _ f) ;
t_subst _ _ (Snd k) _ f := Snd (t_subst _ _ k _ f) ;
t_subst _ _ (Case u v) _ f :=
Case (s_subst _ u _ (a_shift1 f))
(s_subst _ v _ (a_shift1 f))
with w_subst : forallΞA, whn Ξ A -> forallΞ, Ξ =[val]> Ξ -> whn Ξ A :=
w_subst _ _ (VarL i) _ f := f _ i ;
w_subst _ _ (Tt) _ f := Tt ;
w_subst _ _ (Lam u) _ f := Lam (s_subst _ u _ (a_shift3 f)) ;
w_subst _ _ (Pair u v) _ f := Pair (s_subst _ u _ (a_shift1 f))
(s_subst _ v _ (a_shift1 f)) ;
w_subst _ _ (Inl u) _ f := Inl (w_subst _ _ u _ f) ;
w_subst _ _ (Inr u) _ f := Inr (w_subst _ _ u _ f)
with s_subst : state ββ β¦ val , state β§β :=
s_subst _ (Cut v k) _ f := Cut (t_subst _ _ v _ f) (t_subst _ _ k _ f) .Notation"t `ββ a" := (t_subst _ _ t _ a%asgn) (at level30).Notation"w `α΅₯β a" := (w_subst _ _ w _ a%asgn) (at level30).Equationsv_subst : val ββ β¦ val , val β§β :=
v_subst _ β_ v _ f := v `α΅₯β f ;
v_subst _ Β¬_ k _ f := k `ββ f .#[global] Instanceval_monoid : subst_monoid val :=
{| v_var := @Var ; v_sub := v_subst |} .#[global] Instancestate_module : subst_module val state :=
{| c_sub := s_subst |} .Definitionasgn1 {ΞA} (v : val Ξ A) : (Ξ βΆβ A) =[val]> Ξ
:= [ Var ,β v ] .Definitionasgn3 {ΞABC} (v1 : val Ξ A) (v2 : val Ξ B) (v3 : val Ξ C)
: (Ξ βΆβ A βΆβ B βΆβ C) =[val]> Ξ
:= [ [ [ Var ,β v1 ] ,β v2 ] ,β v3 ].Arguments asgn1 {_ _} & _.Arguments asgn3 {_ _ _ _} & _ _.Notation"β[ v ]" := (asgn1 v).Notation"β[ v1 , v2 , v3 ]" := (asgn3 v1 v2 v3).(*Variant forcing0 (Ξ : t_ctx) : pre_ty -> Type :=| FBoom : forcing0 Ξ Zer| FApp {a b} : whn Ξ a -> term Ξ Β¬b -> forcing0 Ξ (a `β b)| FFst {a b} : term Ξ Β¬a -> forcing0 Ξ (a `Γ b)| FSnd {a b} : term Ξ Β¬b -> forcing0 Ξ (a `Γ b)| FCase {a b} : state (Ξ βΆβ βa) -> state (Ξ βΆβ βb) -> forcing0 Ξ (a `+ b).Arguments FBoom {Ξ}.Arguments FApp {Ξ a b}.Arguments FFst {Ξ a b}.Arguments FSnd {Ξ a b}.Arguments FCase {Ξ a b}.Equations f0_subst {Ξ Ξ} : Ξ =[val]> Ξ -> forcing0 Ξ βα΅’ forcing0 Ξ := f0_subst f a (FBoom) := FBoom ; f0_subst f a (FApp v k) := FApp (w_subst f _ v) (t_subst f _ k) ; f0_subst f a (FFst k) := FFst (t_subst f _ k) ; f0_subst f a (FSnd k) := FSnd (t_subst f _ k) ; f0_subst f a (FCase s1 s2) := FCase (s_subst (a_shift1 f) s1) (s_subst (a_shift1 f) s2) .Equations forcing : t_ctx -> ty -> Type := forcing Ξ (t+ a) := whn Ξ a ; forcing Ξ (t- a) := forcing0 Ξ a .Equations f_subst {Ξ Ξ} : Ξ =[val]> Ξ -> forcing Ξ βα΅’ forcing Ξ := f_subst s (t+ a) v := w_subst s a v ; f_subst s (t- a) f := f0_subst s a f .*)Equationsis_neg_pre : pre_ty -> SProp :=
is_neg_pre `0 := sEmpty ;
is_neg_pre `1 := sUnit ;
is_neg_pre (_ `Γ _) := sUnit ;
is_neg_pre (_ `+ _) := sEmpty ;
is_neg_pre (_ `β _) := sUnit .Equationsis_neg : ty -> SProp :=
is_neg βa := is_neg_pre a ;
is_neg Β¬a := sUnit .Definitionneg_ty : Type := sigS is_neg.Definitionneg_coe : neg_ty -> ty := sub_elt.Global Coercionneg_coe : neg_ty >-> ty.Definitionneg_ctx : Type := ctxS ty t_ctx is_neg.Definitionneg_c_coe : neg_ctx -> ctx ty := sub_elt.Global Coercionneg_c_coe : neg_ctx >-> ctx.Bind Scope ctx_scope with neg_ctx.Bind Scope ctx_scope with ctx.Inductivepat : ty -> Type :=
| PTt : pat β`1
| PPair {a b} : pat β(a `Γ b)
| PInl {a b} : pat βa -> pat β(a `+ b)
| PInr {a b} : pat βb -> pat β(a `+ b)
| PLam {a b} : pat β(a `β b)
| PFst {a b} : pat Β¬(a `Γ b)
| PSnd {a b} : pat Β¬(a `Γ b)
| PApp {a b} : pat βa -> pat Β¬(a `β b)
.Equationspat_dom {t} : pat t -> neg_ctx :=
pat_dom (PInl u) := pat_dom u ;
pat_dom (PInr u) := pat_dom u ;
pat_dom (PTt) := β β βΆβ {| sub_elt := β`1 ; sub_prf := stt |} ;
pat_dom (@PLam a b) := β β βΆβ {| sub_elt := β(a `β b) ; sub_prf := stt |} ;
pat_dom (@PPair a b) := β β βΆβ {| sub_elt := β(a `Γ b) ; sub_prf := stt |} ;
pat_dom (@PApp a b v) := pat_dom v βΆβ {| sub_elt := Β¬b ; sub_prf := stt |} ;
pat_dom (@PFst a b) := β β βΆβ {| sub_elt := Β¬a ; sub_prf := stt |} ;
pat_dom (@PSnd a b) := β β βΆβ {| sub_elt := Β¬b ; sub_prf := stt |} .Definitionop_pat : Oper ty neg_ctx :=
{| o_op a := pat a ; o_dom _ p := (pat_dom p) |} .Definitionop_copat : Oper ty neg_ctx :=
{| o_op a := pat (t_neg a) ; o_dom _ p := (pat_dom p) |} .Definitionbare_copat := op_copatβ .Equationsv_of_p {A} (p : pat A) : val (pat_dom p) A :=
v_of_p (PInl u) := Inl (v_of_p u) ;
v_of_p (PInr u) := Inr (v_of_p u) ;
v_of_p (PTt) := VarL top ;
v_of_p (PLam) := VarL top ;
v_of_p (PPair) := VarL top ;
v_of_p (PApp v) := App (v_shift1 _ (v_of_p v)) (VarR top) ;
v_of_p (PFst) := Fst (VarR top) ;
v_of_p (PSnd) := Snd (VarR top) .Coercionv_of_p : pat >-> val.Definitionelim_var_zer {A : Type} {Ξ : neg_ctx} (i : Ξ β β `0) : A
:= match s_prf i withend .Definitionelim_var_sum {A : Type} {Ξ : neg_ctx} {st} (i : Ξ β β (s `+ t)) : A
:= match s_prf i withend .Equationsp_of_w {Ξ : neg_ctx} a : whn Ξ a -> pat βa :=
p_of_w (`0) (VarL i) := elim_var_zer i ;
p_of_w (a `+ b) (VarL i) := elim_var_sum i ;
p_of_w (a `+ b) (Inl v) := PInl (p_of_w _ v) ;
p_of_w (a `+ b) (Inr v) := PInr (p_of_w _ v) ;
p_of_w (`1) _ := PTt ;
p_of_w (a `Γ b) _ := PPair ;
p_of_w (a `β b) _ := PLam .Equationsp_dom_of_w {Ξ : neg_ctx} a (v : whn Ξ a) : pat_dom (p_of_w a v) =[val]> Ξ :=
p_dom_of_w (`0) (VarL i) := elim_var_zer i ;
p_dom_of_w (a `+ b) (VarL i) := elim_var_sum i ;
p_dom_of_w (a `+ b) (Inl v) := p_dom_of_w a v ;
p_dom_of_w (a `+ b) (Inr v) := p_dom_of_w b v ;
p_dom_of_w (`1) v := [ ! ,β v ] ;
p_dom_of_w (a `β b) v := [ ! ,β v ] ;
p_dom_of_w (a `Γ b) v := [ ! ,β v ] .Program Definitionw_split {Ξ : neg_ctx} a (v : whn Ξ a) : (op_copat # val) Ξ Β¬a
:= p_of_w _ v β¦ p_dom_of_w _ v β¦ .DefinitionL_nf : Famβ ty neg_ctx := c_var β₯β (op_copat # val ).(*Definition n_rename {Ξ Ξ : neg_ctx} : Ξ β Ξ -> L_nf Ξ -> L_nf Ξ := fun r n => r _ (nf_var n) β nf_obs n β¦ a_ren r (nf_args n) β¦.*)(*Definition nf0_eq {Ξ a} : relation (nf0 Ξ a) := fun a b => exists H : projT1 a = projT1 b, rew H in projT2 a β‘β projT2 b .Definition nf_eq {Ξ} : relation (nf Ξ) := fun a b => exists H : projT1 a = projT1 b, (rew H in fst (projT2 a) = fst (projT2 b)) /\ (nf0_eq (rew H in snd (projT2 a)) (snd (projT2 b))).#[global] Instance nf0_eq_rfl {Ξ t} : Reflexive (@nf0_eq Ξ t) . intros [ m a ]; unshelve econstructor; auto.Qed.#[global] Instance nf0_eq_sym {Ξ t} : Symmetric (@nf0_eq Ξ t) . intros [ m1 a1 ] [ m2 a2 ] [ p q ]; unshelve econstructor; cbn in *. - now symmetry. - revert a1 q ; rewrite p; intros a1 q. now symmetry.Qed.#[global] Instance nf0_eq_tra {Ξ t} : Transitive (@nf0_eq Ξ t) . intros [ m1 a1 ] [ m2 a2 ] [ m3 a3 ] [ p1 q1 ] [ p2 q2 ]; unshelve econstructor; cbn in *. - now transitivity m2. - transitivity (rew [fun p : pat (t_neg t) => pat_dom p =[ val ]> Ξ] p2 in a2); auto. now rewrite <- p2.Qed.#[global] Instance nf_eq_rfl {Ξ} : Reflexiveα΅’ (fun _ : T1 => @nf_eq Ξ) . intros _ [ x [ i n ] ]. unshelve econstructor; auto.Qed.#[global] Instance nf_eq_sym {Ξ} : Symmetricα΅’ (fun _ : T1 => @nf_eq Ξ) . intros _ [ x1 [ i1 n1 ] ] [ x2 [ i2 n2 ] ] [ p [ q1 q2 ] ]. unshelve econstructor; [ | split ]; cbn in *. - now symmetry. - revert i1 q1; rewrite p; intros i1 q1; now symmetry. - revert n1 q2; rewrite p; intros n1 q2; now symmetry.Qed.#[global] Instance nf_eq_tra {Ξ} : Transitiveα΅’ (fun _ : T1 => @nf_eq Ξ) . intros _ [ x1 [ i1 n1 ] ] [ x2 [ i2 n2 ] ] [ x3 [ i3 n3 ] ] [ p1 [ q1 r1 ] ] [ p2 [ q2 r2 ] ]. unshelve econstructor; [ | split ]; cbn in *. - now transitivity x2. - transitivity (rew [has Ξ] p2 in i2); auto. now rewrite <- p2. - transitivity (rew [nf0 Ξ] p2 in n2); auto. now rewrite <- p2.Qed.Definition comp_eq {Ξ} : relation (delay (nf Ξ)) := it_eq (fun _ : T1 => nf_eq) (i := T1_0) .Notation "u β v" := (comp_eq u v) (at level 40) .Definition pat_of_nf : nf βα΅’ pat' := fun Ξ u => (projT1 u ,' (fst (projT2 u) , projT1 (snd (projT2 u)))) .*)Program Definitionapp_nf {Ξ : neg_ctx} {ab} (i : Ξ β β(a `β b))
(v : whn Ξ a) (k : term Ξ Β¬b) : L_nf Ξ
:= i β PApp (p_of_w _ v) β¦ [ p_dom_of_w _ v ,β (k : val _ Β¬_) ] β¦ .Program Definitionfst_nf {Ξ : neg_ctx} {ab} (i : Ξ β β(a `Γ b))
(k : term Ξ Β¬a) : L_nf Ξ
:= i β PFst β¦ [ ! ,β (k : val _ Β¬_) ] β¦ .Program Definitionsnd_nf {Ξ : neg_ctx} {ab} (i : Ξ β β(a `Γ b))
(k : term Ξ Β¬b) : L_nf Ξ
:= i β PSnd β¦ [ ! ,β (k : val _ Β¬_) ] β¦ .Equationseval_aux {Ξ : neg_ctx} : state Ξ -> (state Ξ + L_nf Ξ) :=
eval_aux (Cut (Mu s) (k)) := inl (s ββ β[ k ]) ;
eval_aux (Cut (Val v) (MuT s)) := inl (s ββ β[ v ]) ;
eval_aux (Cut (Val v) (VarR i)) := inr (s_var_upg i β w_split _ v) ;
eval_aux (Cut (Val (VarL i)) (Boom)) := elim_var_zer i ;
eval_aux (Cut (Val (VarL i)) (Case s t)) := elim_var_sum i ;
eval_aux (Cut (Val (VarL i)) (App v k)) := inr (app_nf i v k) ;
eval_aux (Cut (Val (VarL i)) (Fst k)) := inr (fst_nf i k) ;
eval_aux (Cut (Val (VarL i)) (Snd k)) := inr (snd_nf i k) ;
eval_aux (Cut (Val (Lam s)) (App v k)) := inl (s ββ β[ Lam s , v , k ]) ;
eval_aux (Cut (Val (Pair s t)) (Fst k)) := inl (s ββ β[ k ]) ;
eval_aux (Cut (Val (Pair s t)) (Snd k)) := inl (t ββ β[ k ]) ;
eval_aux (Cut (Val (Inl u)) (Case s t)) := inl (s ββ β[ u ]) ;
eval_aux (Cut (Val (Inr u)) (Case s t)) := inl (t ββ β[ u ]) .Definitioneval {Ξ : neg_ctx} : state Ξ -> delay (L_nf Ξ)
:= iter_delay (func => Ret' (eval_aux c)).(*Definition refold {Ξ : neg_ctx} (p : nf Ξ) : (Ξ β (projT1 p) * val Ξ (t_neg (projT1 p)))%type.destruct p as [x [i [ p s ]]]; cbn in *.exact (i , v_subst s _ (v_of_p p)).Defined.*)Definitionp_app {ΞA} (v : val Ξ A) (m : pat Aβ ) (e : pat_dom m =[val]> Ξ) : state Ξ
:= Cut' v (m `ββ e) .(*Definition emb {Ξ} (m : pat' Ξ) : state (Ξ +βΆβ pat_dom' Ξ m) . destruct m as [a [i v]]; cbn in *. destruct a. - refine (Cut _ _). + refine (Val (VarL (r_concat_l _ i))). + refine (t_rename r_concat_r _ (v_of_p v)). - refine (Cut _ _). + refine (Val (v_rename r_concat_r _ (v_of_p v))). + refine (VarR (r_concat_l _ i)).Defined.*)Schemeterm_mut := Induction for term SortPropwith whn_mut := Induction for whn SortPropwith state_mut := Induction for state SortProp.Recordsyn_ind_args (Pt : forallΞA, term Ξ A -> Prop)
(Pv : forallΞA, whn Ξ A -> Prop)
(Ps : forallΞ, state Ξ -> Prop) :=
{
ind_s_mu : forallΞAs, Ps _ s -> Pt Ξ βA (Mu s) ;
ind_s_val : forallΞAv, Pv _ _ v -> Pt Ξ βA (Val v) ;
ind_s_varn : forallΞAi, Pt Ξ Β¬A (VarR i) ;
ind_s_mut : forallΞAs, Ps _ s -> Pt Ξ Β¬A (MuT s) ;
ind_s_zer : forallΞ, Pt Ξ Β¬`0 Boom ;
ind_s_app : forallΞAB, forallv, Pv _ _ v -> forallk, Pt _ _ k -> Pt Ξ Β¬(A `β B) (App v k) ;
ind_s_fst : forallΞAB, forallk, Pt _ _ k -> Pt Ξ Β¬(A `Γ B) (Fst k) ;
ind_s_snd : forallΞAB, forallk, Pt _ _ k -> Pt Ξ Β¬(A `Γ B) (Snd k) ;
ind_s_match : forallΞAB, foralls, Ps _ s -> forallt, Ps _ t -> Pt Ξ Β¬(A `+ B) (Case s t) ;
ind_s_varp : forallΞAi, Pv Ξ A (VarL i) ;
ind_s_inl : forallΞABv, Pv _ _ v -> Pv Ξ (A `+ B) (Inl v) ;
ind_s_inr : forallΞABv, Pv _ _ v -> Pv Ξ (A `+ B) (Inr v) ;
ind_s_onei : forallΞ, Pv Ξ `1 Tt ;
ind_s_lam : forallΞABs, Ps _ s -> Pv Ξ (A `β B) (Lam s) ;
ind_s_pair : forallΞAB, foralls, Ps _ s -> forallt, Ps _ t -> Pv Ξ (A `Γ B) (Pair s t) ;
ind_s_cut : forallΞA, forallu, Pt _ _ u -> forallv, Pt _ _ v -> Ps Ξ (@Cut _ A u v)
} .
Pt: forall (Ξ : t_ctx) (A : ty), term Ξ A -> Prop Pv: forall (Ξ : t_ctx) (A : pre_ty), whn Ξ A -> Prop Ps: forallΞ : t_ctx, state Ξ -> Prop arg: syn_ind_args Pt Pv Ps Ξ: t_ctx A: ty u: term Ξ A
Pt Ξ A u
destruct arg; nowapply (term_mut Pt Pv Ps).Qed.
Pt: forall (Ξ : t_ctx) (A : ty), term Ξ A -> Prop Pv: forall (Ξ : t_ctx) (A : pre_ty), whn Ξ A -> Prop Ps: forallΞ : t_ctx, state Ξ -> Prop arg: syn_ind_args Pt Pv Ps Ξ: t_ctx A: pre_ty v: whn Ξ A
Pv Ξ A v
destruct arg; nowapply (whn_mut Pt Pv Ps).Qed.
Pt: forall (Ξ : t_ctx) (A : ty), term Ξ A -> Prop Pv: forall (Ξ : t_ctx) (A : pre_ty), whn Ξ A -> Prop Ps: forallΞ : t_ctx, state Ξ -> Prop arg: syn_ind_args Pt Pv Ps Ξ: t_ctx s: state Ξ
Ps Ξ s
destruct arg; nowapply (state_mut Pt Pv Ps).Qed.Definitiont_ren_proper_PΞA (t : term Ξ A) : Prop :=
forallΞ (f1f2 : Ξ β Ξ), f1 β‘β f2 -> t ββα΅£ f1 = t ββα΅£ f2 .Definitionw_ren_proper_PΞA (v : whn Ξ A) : Prop :=
forallΞ (f1f2 : Ξ β Ξ), f1 β‘β f2 -> v `α΅₯βα΅£ f1 = v `α΅₯βα΅£ f2 .Definitions_ren_proper_PΞ (s : state Ξ) : Prop :=
forallΞ (f1f2 : Ξ β Ξ), f1 β‘β f2 -> s ββα΅£ f1 = s ββα΅£ f2 .
forall (Ξ : t_ctx) (A : pre_ty) (s : state (Ξ βΆβ Β¬ A)),
s_ren_proper_P (Ξ βΆβ Β¬ A) s ->
t_ren_proper_P Ξ β A (Mu s)
forall (Ξ : t_ctx) (A : pre_ty) (v : whn Ξ A),
w_ren_proper_P Ξ A v -> t_ren_proper_P Ξ β A (Val v)
forall (Ξ : t_ctx) (A : pre_ty) (i : Ξ β Β¬ A),
t_ren_proper_P Ξ Β¬ A (VarR i)
forall (Ξ : t_ctx) (A : pre_ty) (s : state (Ξ βΆβ β A)),
s_ren_proper_P (Ξ βΆβ β A) s ->
t_ren_proper_P Ξ Β¬ A (MuT s)
forallΞ : t_ctx, t_ren_proper_P Ξ Β¬ `0 Boom
forall (Ξ : t_ctx) (AB : pre_ty) (v : whn Ξ A),
w_ren_proper_P Ξ A v ->
forallk : term Ξ Β¬ B,
t_ren_proper_P Ξ Β¬ B k ->
t_ren_proper_P Ξ Β¬ (A `β B) (App v k)
forall (Ξ : t_ctx) (AB : pre_ty) (k : term Ξ Β¬ A),
t_ren_proper_P Ξ Β¬ A k ->
t_ren_proper_P Ξ Β¬ (A `Γ B) (Fst k)
forall (Ξ : t_ctx) (AB : pre_ty) (k : term Ξ Β¬ B),
t_ren_proper_P Ξ Β¬ B k ->
t_ren_proper_P Ξ Β¬ (A `Γ B) (Snd k)
forall (Ξ : t_ctx) (AB : pre_ty)
(s : state (Ξ βΆβ β A)),
s_ren_proper_P (Ξ βΆβ β A) s ->
forallt : state (Ξ βΆβ β B),
s_ren_proper_P (Ξ βΆβ β B) t ->
t_ren_proper_P Ξ Β¬ (A `+ B) (Case s t)
forall (Ξ : t_ctx) (A : pre_ty) (i : Ξ β β A),
w_ren_proper_P Ξ A (VarL i)
forall (Ξ : t_ctx) (AB : pre_ty) (v : whn Ξ A),
w_ren_proper_P Ξ A v ->
w_ren_proper_P Ξ (A `+ B) (Inl v)
forall (Ξ : t_ctx) (AB : pre_ty) (v : whn Ξ B),
w_ren_proper_P Ξ B v ->
w_ren_proper_P Ξ (A `+ B) (Inr v)
forallΞ : t_ctx, w_ren_proper_P Ξ `1 Tt
forall (Ξ : t_ctx) (AB : pre_ty)
(s : state (Ξ βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B)),
s_ren_proper_P (Ξ βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B) s ->
w_ren_proper_P Ξ (A `β B) (Lam s)
forall (Ξ : t_ctx) (AB : pre_ty)
(s : state (Ξ βΆβ Β¬ A)),
s_ren_proper_P (Ξ βΆβ Β¬ A) s ->
forallt : state (Ξ βΆβ Β¬ B),
s_ren_proper_P (Ξ βΆβ Β¬ B) t ->
w_ren_proper_P Ξ (A `Γ B) (Pair s t)
forall (Ξ : t_ctx) (A : pre_ty) (u : term Ξ β A),
t_ren_proper_P Ξ β A u ->
forallv : term Ξ Β¬ A,
t_ren_proper_P Ξ Β¬ A v -> s_ren_proper_P Ξ (Cut u v)
forall (Ξ : t_ctx) (A : pre_ty) (s : state (Ξ βΆβ Β¬ A)),
(forall (Ξ : t_ctx) (f1f2 : (Ξ βΆβ Β¬ A) β Ξ),
f1 β‘β f2 -> s ββα΅£ f1 = s ββα΅£ f2) ->
forall (Ξ : t_ctx) (f1f2 : Ξ β Ξ),
f1 β‘β f2 -> Mu s ββα΅£ f1 = Mu s ββα΅£ f2
forall (Ξ : t_ctx) (A : pre_ty) (v : whn Ξ A),
(forall (Ξ : t_ctx) (f1f2 : Ξ β Ξ),
f1 β‘β f2 -> v `α΅₯βα΅£ f1 = v `α΅₯βα΅£ f2) ->
forall (Ξ : t_ctx) (f1f2 : Ξ β Ξ),
f1 β‘β f2 -> Val v ββα΅£ f1 = Val v ββα΅£ f2
forall (Ξ : t_ctx) (A : pre_ty) (i : Ξ β Β¬ A)
(Ξ : t_ctx) (f1f2 : Ξ β Ξ),
f1 β‘β f2 -> VarR i ββα΅£ f1 = VarR i ββα΅£ f2
forall (Ξ : t_ctx) (A : pre_ty) (s : state (Ξ βΆβ β A)),
(forall (Ξ : t_ctx) (f1f2 : (Ξ βΆβ β A) β Ξ),
f1 β‘β f2 -> s ββα΅£ f1 = s ββα΅£ f2) ->
forall (Ξ : t_ctx) (f1f2 : Ξ β Ξ),
f1 β‘β f2 -> MuT s ββα΅£ f1 = MuT s ββα΅£ f2
forall (ΞΞ : t_ctx) (f1f2 : Ξ β Ξ),
f1 β‘β f2 -> Boom ββα΅£ f1 = Boom ββα΅£ f2
forall (Ξ : t_ctx) (AB : pre_ty) (v : whn Ξ A),
(forall (Ξ : t_ctx) (f1f2 : Ξ β Ξ),
f1 β‘β f2 -> v `α΅₯βα΅£ f1 = v `α΅₯βα΅£ f2) ->
forallk : term Ξ Β¬ B,
(forall (Ξ : t_ctx) (f1f2 : Ξ β Ξ),
f1 β‘β f2 -> k ββα΅£ f1 = k ββα΅£ f2) ->
forall (Ξ : t_ctx) (f1f2 : Ξ β Ξ),
f1 β‘β f2 -> App v k ββα΅£ f1 = App v k ββα΅£ f2
forall (Ξ : t_ctx) (AB : pre_ty) (k : term Ξ Β¬ A),
(forall (Ξ : t_ctx) (f1f2 : Ξ β Ξ),
f1 β‘β f2 -> k ββα΅£ f1 = k ββα΅£ f2) ->
forall (Ξ : t_ctx) (f1f2 : Ξ β Ξ),
f1 β‘β f2 -> Fst k ββα΅£ f1 = Fst k ββα΅£ f2
forall (Ξ : t_ctx) (AB : pre_ty) (k : term Ξ Β¬ B),
(forall (Ξ : t_ctx) (f1f2 : Ξ β Ξ),
f1 β‘β f2 -> k ββα΅£ f1 = k ββα΅£ f2) ->
forall (Ξ : t_ctx) (f1f2 : Ξ β Ξ),
f1 β‘β f2 -> Snd k ββα΅£ f1 = Snd k ββα΅£ f2
forall (Ξ : t_ctx) (AB : pre_ty)
(s : state (Ξ βΆβ β A)),
(forall (Ξ : t_ctx) (f1f2 : (Ξ βΆβ β A) β Ξ),
f1 β‘β f2 -> s ββα΅£ f1 = s ββα΅£ f2) ->
forallt : state (Ξ βΆβ β B),
(forall (Ξ : t_ctx) (f1f2 : (Ξ βΆβ β B) β Ξ),
f1 β‘β f2 -> t ββα΅£ f1 = t ββα΅£ f2) ->
forall (Ξ : t_ctx) (f1f2 : Ξ β Ξ),
f1 β‘β f2 -> Case s t ββα΅£ f1 = Case s t ββα΅£ f2
forall (Ξ : t_ctx) (A : pre_ty) (i : Ξ β β A)
(Ξ : t_ctx) (f1f2 : Ξ β Ξ),
f1 β‘β f2 -> VarL i `α΅₯βα΅£ f1 = VarL i `α΅₯βα΅£ f2
forall (Ξ : t_ctx) (AB : pre_ty) (v : whn Ξ A),
(forall (Ξ : t_ctx) (f1f2 : Ξ β Ξ),
f1 β‘β f2 -> v `α΅₯βα΅£ f1 = v `α΅₯βα΅£ f2) ->
forall (Ξ : t_ctx) (f1f2 : Ξ β Ξ),
f1 β‘β f2 -> Inl v `α΅₯βα΅£ f1 = Inl v `α΅₯βα΅£ f2
forall (Ξ : t_ctx) (AB : pre_ty) (v : whn Ξ B),
(forall (Ξ : t_ctx) (f1f2 : Ξ β Ξ),
f1 β‘β f2 -> v `α΅₯βα΅£ f1 = v `α΅₯βα΅£ f2) ->
forall (Ξ : t_ctx) (f1f2 : Ξ β Ξ),
f1 β‘β f2 -> Inr v `α΅₯βα΅£ f1 = Inr v `α΅₯βα΅£ f2
forall (ΞΞ : t_ctx) (f1f2 : Ξ β Ξ),
f1 β‘β f2 -> Tt `α΅₯βα΅£ f1 = Tt `α΅₯βα΅£ f2
forall (Ξ : t_ctx) (AB : pre_ty)
(s : state (Ξ βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B)),
(forall (Ξ : t_ctx)
(f1f2 : (Ξ βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B) β Ξ),
f1 β‘β f2 -> s ββα΅£ f1 = s ββα΅£ f2) ->
forall (Ξ : t_ctx) (f1f2 : Ξ β Ξ),
f1 β‘β f2 -> Lam s `α΅₯βα΅£ f1 = Lam s `α΅₯βα΅£ f2
forall (Ξ : t_ctx) (AB : pre_ty)
(s : state (Ξ βΆβ Β¬ A)),
(forall (Ξ : t_ctx) (f1f2 : (Ξ βΆβ Β¬ A) β Ξ),
f1 β‘β f2 -> s ββα΅£ f1 = s ββα΅£ f2) ->
forallt : state (Ξ βΆβ Β¬ B),
(forall (Ξ : t_ctx) (f1f2 : (Ξ βΆβ Β¬ B) β Ξ),
f1 β‘β f2 -> t ββα΅£ f1 = t ββα΅£ f2) ->
forall (Ξ : t_ctx) (f1f2 : Ξ β Ξ),
f1 β‘β f2 -> Pair s t `α΅₯βα΅£ f1 = Pair s t `α΅₯βα΅£ f2
forall (Ξ : t_ctx) (A : pre_ty) (u : term Ξ β A),
(forall (Ξ : t_ctx) (f1f2 : Ξ β Ξ),
f1 β‘β f2 -> u ββα΅£ f1 = u ββα΅£ f2) ->
forallv : term Ξ Β¬ A,
(forall (Ξ : t_ctx) (f1f2 : Ξ β Ξ),
f1 β‘β f2 -> v ββα΅£ f1 = v ββα΅£ f2) ->
forall (Ξ : t_ctx) (f1f2 : Ξ β Ξ),
f1 β‘β f2 -> Cut u v ββα΅£ f1 = Cut u v ββα΅£ f2
Ξ: t_ctx A: pre_ty s: state (Ξ βΆβ Β¬ A) H: forall (Ξ : t_ctx) (f1f2 : (Ξ βΆβ Β¬ A) β Ξ),
f1 β‘β f2 -> s ββα΅£ f1 = s ββα΅£ f2 Ξ: t_ctx f1, f2: Ξ β Ξ H0: f1 β‘β f2
s ββα΅£ r_shift1 f1 = s ββα΅£ r_shift1 f2
Ξ: t_ctx A: pre_ty i: Ξ β Β¬ A Ξ: t_ctx f1, f2: Ξ β Ξ H: f1 β‘β f2
f1 Β¬ A i = f2 Β¬ A i
Ξ: t_ctx A: pre_ty s: state (Ξ βΆβ β A) H: forall (Ξ : t_ctx) (f1f2 : (Ξ βΆβ β A) β Ξ),
f1 β‘β f2 -> s ββα΅£ f1 = s ββα΅£ f2 Ξ: t_ctx f1, f2: Ξ β Ξ H0: f1 β‘β f2
s ββα΅£ r_shift1 f1 = s ββα΅£ r_shift1 f2
Ξ: t_ctx A, B: pre_ty s: state (Ξ βΆβ β A) H: forall (Ξ : t_ctx) (f1f2 : (Ξ βΆβ β A) β Ξ),
f1 β‘β f2 -> s ββα΅£ f1 = s ββα΅£ f2 t: state (Ξ βΆβ β B) H0: forall (Ξ : t_ctx) (f1f2 : (Ξ βΆβ β B) β Ξ),
f1 β‘β f2 -> t ββα΅£ f1 = t ββα΅£ f2 Ξ: t_ctx f1, f2: Ξ β Ξ H1: f1 β‘β f2
s ββα΅£ r_shift1 f1 = s ββα΅£ r_shift1 f2
Ξ: t_ctx A, B: pre_ty s: state (Ξ βΆβ β A) H: forall (Ξ : t_ctx) (f1f2 : (Ξ βΆβ β A) β Ξ),
f1 β‘β f2 -> s ββα΅£ f1 = s ββα΅£ f2 t: state (Ξ βΆβ β B) H0: forall (Ξ : t_ctx) (f1f2 : (Ξ βΆβ β B) β Ξ),
f1 β‘β f2 -> t ββα΅£ f1 = t ββα΅£ f2 Ξ: t_ctx f1, f2: Ξ β Ξ H1: f1 β‘β f2
t ββα΅£ r_shift1 f1 = t ββα΅£ r_shift1 f2
Ξ: t_ctx A: pre_ty i: Ξ β β A Ξ: t_ctx f1, f2: Ξ β Ξ H: f1 β‘β f2
f1 β A i = f2 β A i
Ξ: t_ctx A, B: pre_ty s: state (Ξ βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B) H: forall (Ξ : t_ctx)
(f1f2 : (Ξ βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B) β Ξ),
f1 β‘β f2 -> s ββα΅£ f1 = s ββα΅£ f2 Ξ: t_ctx f1, f2: Ξ β Ξ H0: f1 β‘β f2
s ββα΅£ r_shift3 f1 = s ββα΅£ r_shift3 f2
Ξ: t_ctx A, B: pre_ty s: state (Ξ βΆβ Β¬ A) H: forall (Ξ : t_ctx) (f1f2 : (Ξ βΆβ Β¬ A) β Ξ),
f1 β‘β f2 -> s ββα΅£ f1 = s ββα΅£ f2 t: state (Ξ βΆβ Β¬ B) H0: forall (Ξ : t_ctx) (f1f2 : (Ξ βΆβ Β¬ B) β Ξ),
f1 β‘β f2 -> t ββα΅£ f1 = t ββα΅£ f2 Ξ: t_ctx f1, f2: Ξ β Ξ H1: f1 β‘β f2
s ββα΅£ r_shift1 f1 = s ββα΅£ r_shift1 f2
Ξ: t_ctx A, B: pre_ty s: state (Ξ βΆβ Β¬ A) H: forall (Ξ : t_ctx) (f1f2 : (Ξ βΆβ Β¬ A) β Ξ),
f1 β‘β f2 -> s ββα΅£ f1 = s ββα΅£ f2 t: state (Ξ βΆβ Β¬ B) H0: forall (Ξ : t_ctx) (f1f2 : (Ξ βΆβ Β¬ B) β Ξ),
f1 β‘β f2 -> t ββα΅£ f1 = t ββα΅£ f2 Ξ: t_ctx f1, f2: Ξ β Ξ H1: f1 β‘β f2
t ββα΅£ r_shift1 f1 = t ββα΅£ r_shift1 f2
Ξ: t_ctx A: pre_ty s: state (Ξ βΆβ Β¬ A) H: forall (Ξ : t_ctx) (f1f2 : (Ξ βΆβ Β¬ A) β Ξ),
f1 β‘β f2 -> s ββα΅£ f1 = s ββα΅£ f2 Ξ: t_ctx f1, f2: Ξ β Ξ H0: f1 β‘β f2
s ββα΅£ r_shift1 f1 = s ββα΅£ r_shift1 f2
Ξ: t_ctx A: pre_ty s: state (Ξ βΆβ β A) H: forall (Ξ : t_ctx) (f1f2 : (Ξ βΆβ β A) β Ξ),
f1 β‘β f2 -> s ββα΅£ f1 = s ββα΅£ f2 Ξ: t_ctx f1, f2: Ξ β Ξ H0: f1 β‘β f2
s ββα΅£ r_shift1 f1 = s ββα΅£ r_shift1 f2
Ξ: t_ctx A, B: pre_ty s: state (Ξ βΆβ β A) H: forall (Ξ : t_ctx) (f1f2 : (Ξ βΆβ β A) β Ξ),
f1 β‘β f2 -> s ββα΅£ f1 = s ββα΅£ f2 t: state (Ξ βΆβ β B) H0: forall (Ξ : t_ctx) (f1f2 : (Ξ βΆβ β B) β Ξ),
f1 β‘β f2 -> t ββα΅£ f1 = t ββα΅£ f2 Ξ: t_ctx f1, f2: Ξ β Ξ H1: f1 β‘β f2
s ββα΅£ r_shift1 f1 = s ββα΅£ r_shift1 f2
Ξ: t_ctx A, B: pre_ty s: state (Ξ βΆβ β A) H: forall (Ξ : t_ctx) (f1f2 : (Ξ βΆβ β A) β Ξ),
f1 β‘β f2 -> s ββα΅£ f1 = s ββα΅£ f2 t: state (Ξ βΆβ β B) H0: forall (Ξ : t_ctx) (f1f2 : (Ξ βΆβ β B) β Ξ),
f1 β‘β f2 -> t ββα΅£ f1 = t ββα΅£ f2 Ξ: t_ctx f1, f2: Ξ β Ξ H1: f1 β‘β f2
t ββα΅£ r_shift1 f1 = t ββα΅£ r_shift1 f2
Ξ: t_ctx A, B: pre_ty s: state (Ξ βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B) H: forall (Ξ : t_ctx)
(f1f2 : (Ξ βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B) β Ξ),
f1 β‘β f2 -> s ββα΅£ f1 = s ββα΅£ f2 Ξ: t_ctx f1, f2: Ξ β Ξ H0: f1 β‘β f2
s ββα΅£ r_shift3 f1 = s ββα΅£ r_shift3 f2
Ξ: t_ctx A, B: pre_ty s: state (Ξ βΆβ Β¬ A) H: forall (Ξ : t_ctx) (f1f2 : (Ξ βΆβ Β¬ A) β Ξ),
f1 β‘β f2 -> s ββα΅£ f1 = s ββα΅£ f2 t: state (Ξ βΆβ Β¬ B) H0: forall (Ξ : t_ctx) (f1f2 : (Ξ βΆβ Β¬ B) β Ξ),
f1 β‘β f2 -> t ββα΅£ f1 = t ββα΅£ f2 Ξ: t_ctx f1, f2: Ξ β Ξ H1: f1 β‘β f2
s ββα΅£ r_shift1 f1 = s ββα΅£ r_shift1 f2
Ξ: t_ctx A, B: pre_ty s: state (Ξ βΆβ Β¬ A) H: forall (Ξ : t_ctx) (f1f2 : (Ξ βΆβ Β¬ A) β Ξ),
f1 β‘β f2 -> s ββα΅£ f1 = s ββα΅£ f2 t: state (Ξ βΆβ Β¬ B) H0: forall (Ξ : t_ctx) (f1f2 : (Ξ βΆβ Β¬ B) β Ξ),
f1 β‘β f2 -> t ββα΅£ f1 = t ββα΅£ f2 Ξ: t_ctx f1, f2: Ξ β Ξ H1: f1 β‘β f2
t ββα΅£ r_shift1 f1 = t ββα΅£ r_shift1 f2
Ξ: t_ctx A: pre_ty s: state (Ξ βΆβ Β¬ A) H: forall (Ξ : t_ctx) (f1f2 : (Ξ βΆβ Β¬ A) β Ξ),
f1 β‘β f2 -> s ββα΅£ f1 = s ββα΅£ f2 Ξ: t_ctx f1, f2: Ξ β Ξ H0: f1 β‘β f2
r_shift1 f1 β‘β r_shift1 f2
Ξ: t_ctx A: pre_ty s: state (Ξ βΆβ β A) H: forall (Ξ : t_ctx) (f1f2 : (Ξ βΆβ β A) β Ξ),
f1 β‘β f2 -> s ββα΅£ f1 = s ββα΅£ f2 Ξ: t_ctx f1, f2: Ξ β Ξ H0: f1 β‘β f2
r_shift1 f1 β‘β r_shift1 f2
Ξ: t_ctx A, B: pre_ty s: state (Ξ βΆβ β A) H: forall (Ξ : t_ctx) (f1f2 : (Ξ βΆβ β A) β Ξ),
f1 β‘β f2 -> s ββα΅£ f1 = s ββα΅£ f2 t: state (Ξ βΆβ β B) H0: forall (Ξ : t_ctx) (f1f2 : (Ξ βΆβ β B) β Ξ),
f1 β‘β f2 -> t ββα΅£ f1 = t ββα΅£ f2 Ξ: t_ctx f1, f2: Ξ β Ξ H1: f1 β‘β f2
r_shift1 f1 β‘β r_shift1 f2
Ξ: t_ctx A, B: pre_ty s: state (Ξ βΆβ β A) H: forall (Ξ : t_ctx) (f1f2 : (Ξ βΆβ β A) β Ξ),
f1 β‘β f2 -> s ββα΅£ f1 = s ββα΅£ f2 t: state (Ξ βΆβ β B) H0: forall (Ξ : t_ctx) (f1f2 : (Ξ βΆβ β B) β Ξ),
f1 β‘β f2 -> t ββα΅£ f1 = t ββα΅£ f2 Ξ: t_ctx f1, f2: Ξ β Ξ H1: f1 β‘β f2
r_shift1 f1 β‘β r_shift1 f2
Ξ: t_ctx A, B: pre_ty s: state (Ξ βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B) H: forall (Ξ : t_ctx)
(f1f2 : (Ξ βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B) β Ξ),
f1 β‘β f2 -> s ββα΅£ f1 = s ββα΅£ f2 Ξ: t_ctx f1, f2: Ξ β Ξ H0: f1 β‘β f2
r_shift3 f1 β‘β r_shift3 f2
Ξ: t_ctx A, B: pre_ty s: state (Ξ βΆβ Β¬ A) H: forall (Ξ : t_ctx) (f1f2 : (Ξ βΆβ Β¬ A) β Ξ),
f1 β‘β f2 -> s ββα΅£ f1 = s ββα΅£ f2 t: state (Ξ βΆβ Β¬ B) H0: forall (Ξ : t_ctx) (f1f2 : (Ξ βΆβ Β¬ B) β Ξ),
f1 β‘β f2 -> t ββα΅£ f1 = t ββα΅£ f2 Ξ: t_ctx f1, f2: Ξ β Ξ H1: f1 β‘β f2
r_shift1 f1 β‘β r_shift1 f2
Ξ: t_ctx A, B: pre_ty s: state (Ξ βΆβ Β¬ A) H: forall (Ξ : t_ctx) (f1f2 : (Ξ βΆβ Β¬ A) β Ξ),
f1 β‘β f2 -> s ββα΅£ f1 = s ββα΅£ f2 t: state (Ξ βΆβ Β¬ B) H0: forall (Ξ : t_ctx) (f1f2 : (Ξ βΆβ Β¬ B) β Ξ),
f1 β‘β f2 -> t ββα΅£ f1 = t ββα΅£ f2 Ξ: t_ctx f1, f2: Ξ β Ξ H1: f1 β‘β f2
r_shift1 f1 β‘β r_shift1 f2
all: first [ apply r_shift1_eq | apply r_shift3_eq ]; auto.Qed.
Ξ: t_ctx a: ty t: term Ξ a Ξ: t_ctx
Proper (asgn_eq Ξ Ξ ==> eq) (t_rename Ξ a t Ξ)
intros f1 f2 H1; nowapply (term_ind_mut _ _ _ ren_proper_prf).Qed.
Ξ: t_ctx a: pre_ty v: whn Ξ a Ξ: t_ctx
Proper (asgn_eq Ξ Ξ ==> eq) (w_rename Ξ a v Ξ)
intros f1 f2 H1; nowapply (whn_ind_mut _ _ _ ren_proper_prf).Qed.
Ξ: t_ctx s: state Ξ Ξ: t_ctx
Proper (asgn_eq Ξ Ξ ==> eq) (s_rename Ξ s Ξ)
intros f1 f2 H1; nowapply (state_ind_mut _ _ _ ren_proper_prf).Qed.
Ξ: t_ctx a: ty v: val Ξ a Ξ: t_ctx
Proper (asgn_eq Ξ Ξ ==> eq) (v_rename Ξ a v Ξ)
Ξ: t_ctx p: pre_ty v: val Ξ β p Ξ: t_ctx
Proper (asgn_eq Ξ Ξ ==> eq) (v_rename Ξ β p v Ξ)
Ξ: t_ctx p: pre_ty v: val Ξ Β¬ p Ξ: t_ctx
Proper (asgn_eq Ξ Ξ ==> eq) (v_rename Ξ Β¬ p v Ξ)
Ξ: t_ctx p: pre_ty v: val Ξ Β¬ p Ξ: t_ctx
Proper (asgn_eq Ξ Ξ ==> eq) (v_rename Ξ Β¬ p v Ξ)
Proper
(asgn_eq Ξ Ξ ==>
asgn_eq (Ξ βΆβ A βΆβ B βΆβ C) (Ξ βΆβ A βΆβ B βΆβ C))
(a_shift3 (C:=C))
Ξ, Ξ: t_ctx A, B, C: ty x, y: Ξ =[ val ]> Ξ H: x β‘β y a: ty v: Ξ βΆβ A βΆβ B βΆβ C β a
a_shift3 x a v = a_shift3 y a v
Ξ1: ctx ty Ξ: t_ctx y2, y1, y0: ty x, y: Ξ1 =[ val ]> Ξ H: x β‘β y a: ty v: var a Ξ1
a_shift3 x a (pop (pop (pop v))) =
a_shift3 y a (pop (pop (pop v)))
cbn; nowrewrite H.Qed.Definitiont_ren_ren_PΞ1A (t : term Ξ1 A) : Prop :=
forallΞ2Ξ3 (f1 : Ξ1 β Ξ2) (f2 : Ξ2 β Ξ3),
(t ββα΅£ f1) ββα΅£ f2 = t ββα΅£ (f1 α΅£β f2) .Definitionw_ren_ren_PΞ1A (v : whn Ξ1 A) : Prop :=
forallΞ2Ξ3 (f1 : Ξ1 β Ξ2) (f2 : Ξ2 β Ξ3),
(v `α΅₯βα΅£ f1) `α΅₯βα΅£ f2 = v `α΅₯βα΅£ (f1 α΅£β f2) .Definitions_ren_ren_PΞ1 (s : state Ξ1) : Prop :=
forallΞ2Ξ3 (f1 : Ξ1 β Ξ2) (f2 : Ξ2 β Ξ3),
(s ββα΅£ f1) ββα΅£ f2 = s ββα΅£ (f1 α΅£β f2) .
syn_ind_args t_ren_ren_P w_ren_ren_P s_ren_ren_P
forall (Ξ : t_ctx) (A : pre_ty) (s : state (Ξ βΆβ Β¬ A)),
s_ren_ren_P (Ξ βΆβ Β¬ A) s -> t_ren_ren_P Ξ β A (Mu s)
forall (Ξ : t_ctx) (A : pre_ty) (v : whn Ξ A),
w_ren_ren_P Ξ A v -> t_ren_ren_P Ξ β A (Val v)
forall (Ξ : t_ctx) (A : pre_ty) (i : Ξ β Β¬ A),
t_ren_ren_P Ξ Β¬ A (VarR i)
forall (Ξ : t_ctx) (A : pre_ty) (s : state (Ξ βΆβ β A)),
s_ren_ren_P (Ξ βΆβ β A) s -> t_ren_ren_P Ξ Β¬ A (MuT s)
forallΞ : t_ctx, t_ren_ren_P Ξ Β¬ `0 Boom
forall (Ξ : t_ctx) (AB : pre_ty) (v : whn Ξ A),
w_ren_ren_P Ξ A v ->
forallk : term Ξ Β¬ B,
t_ren_ren_P Ξ Β¬ B k ->
t_ren_ren_P Ξ Β¬ (A `β B) (App v k)
forall (Ξ : t_ctx) (AB : pre_ty) (k : term Ξ Β¬ A),
t_ren_ren_P Ξ Β¬ A k ->
t_ren_ren_P Ξ Β¬ (A `Γ B) (Fst k)
forall (Ξ : t_ctx) (AB : pre_ty) (k : term Ξ Β¬ B),
t_ren_ren_P Ξ Β¬ B k ->
t_ren_ren_P Ξ Β¬ (A `Γ B) (Snd k)
forall (Ξ : t_ctx) (AB : pre_ty)
(s : state (Ξ βΆβ β A)),
s_ren_ren_P (Ξ βΆβ β A) s ->
forallt : state (Ξ βΆβ β B),
s_ren_ren_P (Ξ βΆβ β B) t ->
t_ren_ren_P Ξ Β¬ (A `+ B) (Case s t)
forall (Ξ : t_ctx) (A : pre_ty) (i : Ξ β β A),
w_ren_ren_P Ξ A (VarL i)
forall (Ξ : t_ctx) (AB : pre_ty) (v : whn Ξ A),
w_ren_ren_P Ξ A v -> w_ren_ren_P Ξ (A `+ B) (Inl v)
forall (Ξ : t_ctx) (AB : pre_ty) (v : whn Ξ B),
w_ren_ren_P Ξ B v -> w_ren_ren_P Ξ (A `+ B) (Inr v)
forallΞ : t_ctx, w_ren_ren_P Ξ `1 Tt
forall (Ξ : t_ctx) (AB : pre_ty)
(s : state (Ξ βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B)),
s_ren_ren_P (Ξ βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B) s ->
w_ren_ren_P Ξ (A `β B) (Lam s)
forall (Ξ : t_ctx) (AB : pre_ty)
(s : state (Ξ βΆβ Β¬ A)),
s_ren_ren_P (Ξ βΆβ Β¬ A) s ->
forallt : state (Ξ βΆβ Β¬ B),
s_ren_ren_P (Ξ βΆβ Β¬ B) t ->
w_ren_ren_P Ξ (A `Γ B) (Pair s t)
forall (Ξ : t_ctx) (A : pre_ty) (u : term Ξ β A),
t_ren_ren_P Ξ β A u ->
forallv : term Ξ Β¬ A,
t_ren_ren_P Ξ Β¬ A v -> s_ren_ren_P Ξ (Cut u v)
forall (Ξ : t_ctx) (A : pre_ty) (s : state (Ξ βΆβ Β¬ A)),
(forall (Ξ2Ξ3 : t_ctx) (f1 : (Ξ βΆβ Β¬ A) β Ξ2)
(f2 : Ξ2 β Ξ3),
(s ββα΅£ f1) ββα΅£ f2 = s ββα΅£ (f1 α΅£β f2)) ->
forall (Ξ2Ξ3 : t_ctx) (f1 : Ξ β Ξ2) (f2 : Ξ2 β Ξ3),
(Mu s ββα΅£ f1) ββα΅£ f2 = Mu s ββα΅£ (f1 α΅£β f2)
forall (Ξ : t_ctx) (A : pre_ty) (v : whn Ξ A),
(forall (Ξ2Ξ3 : t_ctx) (f1 : Ξ β Ξ2) (f2 : Ξ2 β Ξ3),
(v `α΅₯βα΅£ f1) `α΅₯βα΅£ f2 = v `α΅₯βα΅£ (f1 α΅£β f2)) ->
forall (Ξ2Ξ3 : t_ctx) (f1 : Ξ β Ξ2) (f2 : Ξ2 β Ξ3),
(Val v ββα΅£ f1) ββα΅£ f2 = Val v ββα΅£ (f1 α΅£β f2)
forall (Ξ : t_ctx) (A : pre_ty) (i : Ξ β Β¬ A)
(Ξ2Ξ3 : t_ctx) (f1 : Ξ β Ξ2) (f2 : Ξ2 β Ξ3),
(VarR i ββα΅£ f1) ββα΅£ f2 = VarR i ββα΅£ (f1 α΅£β f2)
forall (Ξ : t_ctx) (A : pre_ty) (s : state (Ξ βΆβ β A)),
(forall (Ξ2Ξ3 : t_ctx) (f1 : (Ξ βΆβ β A) β Ξ2)
(f2 : Ξ2 β Ξ3),
(s ββα΅£ f1) ββα΅£ f2 = s ββα΅£ (f1 α΅£β f2)) ->
forall (Ξ2Ξ3 : t_ctx) (f1 : Ξ β Ξ2) (f2 : Ξ2 β Ξ3),
(MuT s ββα΅£ f1) ββα΅£ f2 = MuT s ββα΅£ (f1 α΅£β f2)
Ξ1, Ξ2, Ξ3: ctx ty f1: Ξ1 β Ξ2 f2: Ξ2 β Ξ3 A: pre_ty v: whn Ξ1 A
(v `α΅₯βα΅£ f1) `α΅₯βα΅£ f2 = v `α΅₯βα΅£ (f1 α΅£β f2)
nowapply (whn_ind_mut _ _ _ ren_ren_prf).Qed.
Ξ1, Ξ2, Ξ3: ctx ty f1: Ξ1 β Ξ2 f2: Ξ2 β Ξ3 s: state Ξ1
(s ββα΅£ f1) ββα΅£ f2 = s ββα΅£ (f1 α΅£β f2)
nowapply (state_ind_mut _ _ _ ren_ren_prf).Qed.
Ξ1, Ξ2, Ξ3: ctx ty f1: Ξ1 β Ξ2 f2: Ξ2 β Ξ3 A: ty v: val Ξ1 A
(v α΅₯βα΅£ f1) α΅₯βα΅£ f2 = v α΅₯βα΅£ (f1 α΅£β f2)
Ξ1, Ξ2, Ξ3: ctx ty f1: Ξ1 β Ξ2 f2: Ξ2 β Ξ3 p: pre_ty v: val Ξ1 β p
(v α΅₯βα΅£ f1) α΅₯βα΅£ f2 = v α΅₯βα΅£ (f1 α΅£β f2)
Ξ1, Ξ2, Ξ3: ctx ty f1: Ξ1 β Ξ2 f2: Ξ2 β Ξ3 p: pre_ty v: val Ξ1 Β¬ p
(v α΅₯βα΅£ f1) α΅₯βα΅£ f2 = v α΅₯βα΅£ (f1 α΅£β f2)
Ξ1, Ξ2, Ξ3: ctx ty f1: Ξ1 β Ξ2 f2: Ξ2 β Ξ3 p: pre_ty v: val Ξ1 Β¬ p
(v α΅₯βα΅£ f1) α΅₯βα΅£ f2 = v α΅₯βα΅£ (f1 α΅£β f2)
nowapply t_ren_ren.Qed.Definitiont_ren_id_l_PΞA (t : term Ξ A) : Prop := t ββα΅£ r_id = t.Definitionw_ren_id_l_PΞA (v : whn Ξ A) : Prop := v `α΅₯βα΅£ r_id = v.Definitions_ren_id_l_PΞ (s : state Ξ) : Prop := s ββα΅£ r_id = s.
forall (Ξ : t_ctx) (A : pre_ty) (s : state (Ξ βΆβ Β¬ A)),
s_ren_id_l_P (Ξ βΆβ Β¬ A) s -> t_ren_id_l_P Ξ β A (Mu s)
forall (Ξ : t_ctx) (A : pre_ty) (v : whn Ξ A),
w_ren_id_l_P Ξ A v -> t_ren_id_l_P Ξ β A (Val v)
forall (Ξ : t_ctx) (A : pre_ty) (i : Ξ β Β¬ A),
t_ren_id_l_P Ξ Β¬ A (VarR i)
forall (Ξ : t_ctx) (A : pre_ty) (s : state (Ξ βΆβ β A)),
s_ren_id_l_P (Ξ βΆβ β A) s ->
t_ren_id_l_P Ξ Β¬ A (MuT s)
forallΞ : t_ctx, t_ren_id_l_P Ξ Β¬ `0 Boom
forall (Ξ : t_ctx) (AB : pre_ty) (v : whn Ξ A),
w_ren_id_l_P Ξ A v ->
forallk : term Ξ Β¬ B,
t_ren_id_l_P Ξ Β¬ B k ->
t_ren_id_l_P Ξ Β¬ (A `β B) (App v k)
forall (Ξ : t_ctx) (AB : pre_ty) (k : term Ξ Β¬ A),
t_ren_id_l_P Ξ Β¬ A k ->
t_ren_id_l_P Ξ Β¬ (A `Γ B) (Fst k)
forall (Ξ : t_ctx) (AB : pre_ty) (k : term Ξ Β¬ B),
t_ren_id_l_P Ξ Β¬ B k ->
t_ren_id_l_P Ξ Β¬ (A `Γ B) (Snd k)
forall (Ξ : t_ctx) (AB : pre_ty)
(s : state (Ξ βΆβ β A)),
s_ren_id_l_P (Ξ βΆβ β A) s ->
forallt : state (Ξ βΆβ β B),
s_ren_id_l_P (Ξ βΆβ β B) t ->
t_ren_id_l_P Ξ Β¬ (A `+ B) (Case s t)
forall (Ξ : t_ctx) (A : pre_ty) (i : Ξ β β A),
w_ren_id_l_P Ξ A (VarL i)
forall (Ξ : t_ctx) (AB : pre_ty) (v : whn Ξ A),
w_ren_id_l_P Ξ A v -> w_ren_id_l_P Ξ (A `+ B) (Inl v)
forall (Ξ : t_ctx) (AB : pre_ty) (v : whn Ξ B),
w_ren_id_l_P Ξ B v -> w_ren_id_l_P Ξ (A `+ B) (Inr v)
forallΞ : t_ctx, w_ren_id_l_P Ξ `1 Tt
forall (Ξ : t_ctx) (AB : pre_ty)
(s : state (Ξ βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B)),
s_ren_id_l_P (Ξ βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B) s ->
w_ren_id_l_P Ξ (A `β B) (Lam s)
forall (Ξ : t_ctx) (AB : pre_ty)
(s : state (Ξ βΆβ Β¬ A)),
s_ren_id_l_P (Ξ βΆβ Β¬ A) s ->
forallt : state (Ξ βΆβ Β¬ B),
s_ren_id_l_P (Ξ βΆβ Β¬ B) t ->
w_ren_id_l_P Ξ (A `Γ B) (Pair s t)
forall (Ξ : t_ctx) (A : pre_ty) (u : term Ξ β A),
t_ren_id_l_P Ξ β A u ->
forallv : term Ξ Β¬ A,
t_ren_id_l_P Ξ Β¬ A v -> s_ren_id_l_P Ξ (Cut u v)
forall (Ξ : t_ctx) (A : pre_ty) (s : state (Ξ βΆβ Β¬ A)),
s ββα΅£ r_id = s -> Mu s ββα΅£ r_id = Mu s
forall (Ξ : t_ctx) (A : pre_ty) (v : whn Ξ A),
v `α΅₯βα΅£ r_id = v -> Val v ββα΅£ r_id = Val v
forall (Ξ : t_ctx) (A : pre_ty) (i : Ξ β Β¬ A),
VarR i ββα΅£ r_id = VarR i
forall (Ξ : t_ctx) (A : pre_ty) (s : state (Ξ βΆβ β A)),
s ββα΅£ r_id = s -> MuT s ββα΅£ r_id = MuT s
forallΞ : t_ctx, Boom ββα΅£ r_id = Boom
forall (Ξ : t_ctx) (AB : pre_ty) (v : whn Ξ A),
v `α΅₯βα΅£ r_id = v ->
forallk : term Ξ Β¬ B,
k ββα΅£ r_id = k -> App v k ββα΅£ r_id = App v k
forall (Ξ : t_ctx) (AB : pre_ty) (k : term Ξ Β¬ A),
k ββα΅£ r_id = k -> Fst k ββα΅£ r_id = Fst k
forall (Ξ : t_ctx) (AB : pre_ty) (k : term Ξ Β¬ B),
k ββα΅£ r_id = k -> Snd k ββα΅£ r_id = Snd k
forall (Ξ : t_ctx) (AB : pre_ty)
(s : state (Ξ βΆβ β A)),
s ββα΅£ r_id = s ->
forallt : state (Ξ βΆβ β B),
t ββα΅£ r_id = t -> Case s t ββα΅£ r_id = Case s t
forall (Ξ : t_ctx) (A : pre_ty) (i : Ξ β β A),
VarL i `α΅₯βα΅£ r_id = VarL i
forall (Ξ : t_ctx) (AB : pre_ty) (v : whn Ξ A),
v `α΅₯βα΅£ r_id = v -> Inl v `α΅₯βα΅£ r_id = Inl v
forall (Ξ : t_ctx) (AB : pre_ty) (v : whn Ξ B),
v `α΅₯βα΅£ r_id = v -> Inr v `α΅₯βα΅£ r_id = Inr v
forallΞ : t_ctx, Tt `α΅₯βα΅£ r_id = Tt
forall (Ξ : t_ctx) (AB : pre_ty)
(s : state (Ξ βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B)),
s ββα΅£ r_id = s -> Lam s `α΅₯βα΅£ r_id = Lam s
forall (Ξ : t_ctx) (AB : pre_ty)
(s : state (Ξ βΆβ Β¬ A)),
s ββα΅£ r_id = s ->
forallt : state (Ξ βΆβ Β¬ B),
t ββα΅£ r_id = t -> Pair s t `α΅₯βα΅£ r_id = Pair s t
forall (Ξ : t_ctx) (A : pre_ty) (u : term Ξ β A),
u ββα΅£ r_id = u ->
forallv : term Ξ Β¬ A,
v ββα΅£ r_id = v -> Cut u v ββα΅£ r_id = Cut u v
Ξ: t_ctx A: pre_ty s: state (Ξ βΆβ Β¬ A) H: s ββα΅£ r_id = s
s ββα΅£ r_shift1 r_id = s
Ξ: t_ctx A: pre_ty s: state (Ξ βΆβ β A) H: s ββα΅£ r_id = s
s ββα΅£ r_shift1 r_id = s
Ξ: t_ctx A, B: pre_ty s: state (Ξ βΆβ β A) H: s ββα΅£ r_id = s t: state (Ξ βΆβ β B) H0: t ββα΅£ r_id = t
s ββα΅£ r_shift1 r_id = s
Ξ: t_ctx A, B: pre_ty s: state (Ξ βΆβ β A) H: s ββα΅£ r_id = s t: state (Ξ βΆβ β B) H0: t ββα΅£ r_id = t
t ββα΅£ r_shift1 r_id = t
Ξ: t_ctx A, B: pre_ty s: state (Ξ βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B) H: s ββα΅£ r_id = s
s ββα΅£ r_shift3 r_id = s
Ξ: t_ctx A, B: pre_ty s: state (Ξ βΆβ Β¬ A) H: s ββα΅£ r_id = s t: state (Ξ βΆβ Β¬ B) H0: t ββα΅£ r_id = t
s ββα΅£ r_shift1 r_id = s
Ξ: t_ctx A, B: pre_ty s: state (Ξ βΆβ Β¬ A) H: s ββα΅£ r_id = s t: state (Ξ βΆβ Β¬ B) H0: t ββα΅£ r_id = t
t ββα΅£ r_shift1 r_id = t
all: first [ rewrite r_shift1_id | rewrite r_shift3_id ]; eauto.Qed.
Ξ: t_ctx A, B, C, a: ty v: Ξ βΆβ A βΆβ B βΆβ C β a
a_shift3 Var a v = Var v
Ξ1: ctx ty y1, y0, y, a: ty v: var a Ξ1
v_shift3 a (Var v) = Var (pop (pop (pop v)))
nowdestruct a.Qed.Arguments Var : simpl never.
Ξ1, Ξ2, Ξ3: t_ctx A: ty f1: Ξ1 =[ val ]> Ξ2 f2: Ξ2 β Ξ3
a_shift1 (f1 βα΅£ f2) β‘β a_shift1 f1 βα΅£ r_shift1 f2
Ξ: ctx ty Ξ2, Ξ3: t_ctx a: ty f1: Ξ =[ val ]> Ξ2 f2: Ξ2 β Ξ3
Var top = Var top α΅₯βα΅£ r_shift1 f2
Ξ0: ctx ty Ξ2, Ξ3: t_ctx y: ty f1: Ξ0 =[ val ]> Ξ2 f2: Ξ2 β Ξ3 a: ty v: var a Ξ0
v_shift1 a (f1 a v α΅₯βα΅£ f2) =
v_shift1 a (f1 a v) α΅₯βα΅£ r_shift1 f2
Ξ: ctx ty Ξ2, Ξ3: t_ctx a: ty f1: Ξ =[ val ]> Ξ2 f2: Ξ2 β Ξ3
Var top = Var top α΅₯βα΅£ r_shift1 f2
nowrewrite v_ren_id_r.
Ξ0: ctx ty Ξ2, Ξ3: t_ctx y: ty f1: Ξ0 =[ val ]> Ξ2 f2: Ξ2 β Ξ3 a: ty v: var a Ξ0
v_shift1 a (f1 a v α΅₯βα΅£ f2) =
v_shift1 a (f1 a v) α΅₯βα΅£ r_shift1 f2
nowunfold v_shift1; rewrite2 v_ren_ren.Qed.
Ξ1, Ξ2, Ξ3: t_ctx A, B, C: ty f1: Ξ1 =[ val ]> Ξ2 f2: Ξ2 β Ξ3
a_shift3 (f1 βα΅£ f2) β‘β a_shift3 f1 βα΅£ r_shift3 f2
Ξ0: ctx ty Ξ2, Ξ3: t_ctx y1, y0, y: ty f1: Ξ0 =[ val ]> Ξ2 f2: Ξ2 β Ξ3 a: ty v: var a Ξ0
v_shift3 a (f1 a v α΅₯βα΅£ f2) =
v_shift3 a (f1 a v) α΅₯βα΅£ r_shift3 f2
unfold v_shift3; nowrewrite2 v_ren_ren.Qed.
Ξ1, Ξ2: ctx ty Ξ3: t_ctx A: ty f1: Ξ1 β Ξ2 f2: Ξ2 =[ val ]> Ξ3
a_shift1 (f1 α΅£β f2) β‘β r_shift1 f1 α΅£β a_shift1 f2
intros ? i; dependent elimination i; auto.Qed.
Ξ1, Ξ2: ctx ty Ξ3: t_ctx A, B, C: ty f1: Ξ1 β Ξ2 f2: Ξ2 =[ val ]> Ξ3
a_shift3 (f1 α΅£β f2) β‘β r_shift3 f1 α΅£β a_shift3 f2
intros ? v; do3 (dependent elimination v; auto).Qed.Definitiont_sub_proper_PΞA (t : term Ξ A) : Prop :=
forallΞ (f1f2 : Ξ =[val]> Ξ), f1 β‘β f2 -> t `ββ f1 = t `ββ f2 .Definitionw_sub_proper_PΞA (v : whn Ξ A) : Prop :=
forallΞ (f1f2 : Ξ =[val]> Ξ), f1 β‘β f2 -> v `α΅₯β f1 = v `α΅₯β f2 .Definitions_sub_proper_PΞ (s : state Ξ) : Prop :=
forallΞ (f1f2 : Ξ =[val]> Ξ), f1 β‘β f2 -> s ββ f1 = s ββ f2 .
forall (Ξ : t_ctx) (A : pre_ty) (s : state (Ξ βΆβ Β¬ A)),
s_sub_proper_P (Ξ βΆβ Β¬ A) s ->
t_sub_proper_P Ξ β A (Mu s)
forall (Ξ : t_ctx) (A : pre_ty) (v : whn Ξ A),
w_sub_proper_P Ξ A v -> t_sub_proper_P Ξ β A (Val v)
forall (Ξ : t_ctx) (A : pre_ty) (i : Ξ β Β¬ A),
t_sub_proper_P Ξ Β¬ A (VarR i)
forall (Ξ : t_ctx) (A : pre_ty) (s : state (Ξ βΆβ β A)),
s_sub_proper_P (Ξ βΆβ β A) s ->
t_sub_proper_P Ξ Β¬ A (MuT s)
forallΞ : t_ctx, t_sub_proper_P Ξ Β¬ `0 Boom
forall (Ξ : t_ctx) (AB : pre_ty) (v : whn Ξ A),
w_sub_proper_P Ξ A v ->
forallk : term Ξ Β¬ B,
t_sub_proper_P Ξ Β¬ B k ->
t_sub_proper_P Ξ Β¬ (A `β B) (App v k)
forall (Ξ : t_ctx) (AB : pre_ty) (k : term Ξ Β¬ A),
t_sub_proper_P Ξ Β¬ A k ->
t_sub_proper_P Ξ Β¬ (A `Γ B) (Fst k)
forall (Ξ : t_ctx) (AB : pre_ty) (k : term Ξ Β¬ B),
t_sub_proper_P Ξ Β¬ B k ->
t_sub_proper_P Ξ Β¬ (A `Γ B) (Snd k)
forall (Ξ : t_ctx) (AB : pre_ty)
(s : state (Ξ βΆβ β A)),
s_sub_proper_P (Ξ βΆβ β A) s ->
forallt : state (Ξ βΆβ β B),
s_sub_proper_P (Ξ βΆβ β B) t ->
t_sub_proper_P Ξ Β¬ (A `+ B) (Case s t)
forall (Ξ : t_ctx) (A : pre_ty) (i : Ξ β β A),
w_sub_proper_P Ξ A (VarL i)
forall (Ξ : t_ctx) (AB : pre_ty) (v : whn Ξ A),
w_sub_proper_P Ξ A v ->
w_sub_proper_P Ξ (A `+ B) (Inl v)
forall (Ξ : t_ctx) (AB : pre_ty) (v : whn Ξ B),
w_sub_proper_P Ξ B v ->
w_sub_proper_P Ξ (A `+ B) (Inr v)
forallΞ : t_ctx, w_sub_proper_P Ξ `1 Tt
forall (Ξ : t_ctx) (AB : pre_ty)
(s : state (Ξ βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B)),
s_sub_proper_P (Ξ βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B) s ->
w_sub_proper_P Ξ (A `β B) (Lam s)
forall (Ξ : t_ctx) (AB : pre_ty)
(s : state (Ξ βΆβ Β¬ A)),
s_sub_proper_P (Ξ βΆβ Β¬ A) s ->
forallt : state (Ξ βΆβ Β¬ B),
s_sub_proper_P (Ξ βΆβ Β¬ B) t ->
w_sub_proper_P Ξ (A `Γ B) (Pair s t)
forall (Ξ : t_ctx) (A : pre_ty) (u : term Ξ β A),
t_sub_proper_P Ξ β A u ->
forallv : term Ξ Β¬ A,
t_sub_proper_P Ξ Β¬ A v -> s_sub_proper_P Ξ (Cut u v)
forall (Ξ : t_ctx) (A : pre_ty) (s : state (Ξ βΆβ Β¬ A)),
(forall (Ξ : t_ctx) (f1f2 : (Ξ βΆβ Β¬ A) =[ val ]> Ξ),
f1 β‘β f2 -> s ββ f1 = s ββ f2) ->
forall (Ξ : t_ctx) (f1f2 : Ξ =[ val ]> Ξ),
f1 β‘β f2 -> Mu s `ββ f1 = Mu s `ββ f2
forall (Ξ : t_ctx) (A : pre_ty) (v : whn Ξ A),
(forall (Ξ : t_ctx) (f1f2 : Ξ =[ val ]> Ξ),
f1 β‘β f2 -> v `α΅₯β f1 = v `α΅₯β f2) ->
forall (Ξ : t_ctx) (f1f2 : Ξ =[ val ]> Ξ),
f1 β‘β f2 -> Val v `ββ f1 = Val v `ββ f2
forall (Ξ : t_ctx) (A : pre_ty) (i : Ξ β Β¬ A)
(Ξ : t_ctx) (f1f2 : Ξ =[ val ]> Ξ),
f1 β‘β f2 -> VarR i `ββ f1 = VarR i `ββ f2
forall (Ξ : t_ctx) (A : pre_ty) (s : state (Ξ βΆβ β A)),
(forall (Ξ : t_ctx) (f1f2 : (Ξ βΆβ β A) =[ val ]> Ξ),
f1 β‘β f2 -> s ββ f1 = s ββ f2) ->
forall (Ξ : t_ctx) (f1f2 : Ξ =[ val ]> Ξ),
f1 β‘β f2 -> MuT s `ββ f1 = MuT s `ββ f2
forall (ΞΞ : t_ctx) (f1f2 : Ξ =[ val ]> Ξ),
f1 β‘β f2 -> Boom `ββ f1 = Boom `ββ f2
forall (Ξ : t_ctx) (AB : pre_ty) (v : whn Ξ A),
(forall (Ξ : t_ctx) (f1f2 : Ξ =[ val ]> Ξ),
f1 β‘β f2 -> v `α΅₯β f1 = v `α΅₯β f2) ->
forallk : term Ξ Β¬ B,
(forall (Ξ : t_ctx) (f1f2 : Ξ =[ val ]> Ξ),
f1 β‘β f2 -> k `ββ f1 = k `ββ f2) ->
forall (Ξ : t_ctx) (f1f2 : Ξ =[ val ]> Ξ),
f1 β‘β f2 -> App v k `ββ f1 = App v k `ββ f2
forall (Ξ : t_ctx) (AB : pre_ty) (k : term Ξ Β¬ A),
(forall (Ξ : t_ctx) (f1f2 : Ξ =[ val ]> Ξ),
f1 β‘β f2 -> k `ββ f1 = k `ββ f2) ->
forall (Ξ : t_ctx) (f1f2 : Ξ =[ val ]> Ξ),
f1 β‘β f2 -> Fst k `ββ f1 = Fst k `ββ f2
forall (Ξ : t_ctx) (AB : pre_ty) (k : term Ξ Β¬ B),
(forall (Ξ : t_ctx) (f1f2 : Ξ =[ val ]> Ξ),
f1 β‘β f2 -> k `ββ f1 = k `ββ f2) ->
forall (Ξ : t_ctx) (f1f2 : Ξ =[ val ]> Ξ),
f1 β‘β f2 -> Snd k `ββ f1 = Snd k `ββ f2
forall (Ξ : t_ctx) (AB : pre_ty)
(s : state (Ξ βΆβ β A)),
(forall (Ξ : t_ctx) (f1f2 : (Ξ βΆβ β A) =[ val ]> Ξ),
f1 β‘β f2 -> s ββ f1 = s ββ f2) ->
forallt : state (Ξ βΆβ β B),
(forall (Ξ : t_ctx) (f1f2 : (Ξ βΆβ β B) =[ val ]> Ξ),
f1 β‘β f2 -> t ββ f1 = t ββ f2) ->
forall (Ξ : t_ctx) (f1f2 : Ξ =[ val ]> Ξ),
f1 β‘β f2 -> Case s t `ββ f1 = Case s t `ββ f2
forall (Ξ : t_ctx) (A : pre_ty) (i : Ξ β β A)
(Ξ : t_ctx) (f1f2 : Ξ =[ val ]> Ξ),
f1 β‘β f2 -> VarL i `α΅₯β f1 = VarL i `α΅₯β f2
forall (Ξ : t_ctx) (AB : pre_ty) (v : whn Ξ A),
(forall (Ξ : t_ctx) (f1f2 : Ξ =[ val ]> Ξ),
f1 β‘β f2 -> v `α΅₯β f1 = v `α΅₯β f2) ->
forall (Ξ : t_ctx) (f1f2 : Ξ =[ val ]> Ξ),
f1 β‘β f2 -> Inl v `α΅₯β f1 = Inl v `α΅₯β f2
forall (Ξ : t_ctx) (AB : pre_ty) (v : whn Ξ B),
(forall (Ξ : t_ctx) (f1f2 : Ξ =[ val ]> Ξ),
f1 β‘β f2 -> v `α΅₯β f1 = v `α΅₯β f2) ->
forall (Ξ : t_ctx) (f1f2 : Ξ =[ val ]> Ξ),
f1 β‘β f2 -> Inr v `α΅₯β f1 = Inr v `α΅₯β f2
forall (ΞΞ : t_ctx) (f1f2 : Ξ =[ val ]> Ξ),
f1 β‘β f2 -> Tt `α΅₯β f1 = Tt `α΅₯β f2
forall (Ξ : t_ctx) (AB : pre_ty)
(s : state (Ξ βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B)),
(forall (Ξ : t_ctx)
(f1f2 : (Ξ βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B) =[ val ]> Ξ),
f1 β‘β f2 -> s ββ f1 = s ββ f2) ->
forall (Ξ : t_ctx) (f1f2 : Ξ =[ val ]> Ξ),
f1 β‘β f2 -> Lam s `α΅₯β f1 = Lam s `α΅₯β f2
forall (Ξ : t_ctx) (AB : pre_ty)
(s : state (Ξ βΆβ Β¬ A)),
(forall (Ξ : t_ctx) (f1f2 : (Ξ βΆβ Β¬ A) =[ val ]> Ξ),
f1 β‘β f2 -> s ββ f1 = s ββ f2) ->
forallt : state (Ξ βΆβ Β¬ B),
(forall (Ξ : t_ctx) (f1f2 : (Ξ βΆβ Β¬ B) =[ val ]> Ξ),
f1 β‘β f2 -> t ββ f1 = t ββ f2) ->
forall (Ξ : t_ctx) (f1f2 : Ξ =[ val ]> Ξ),
f1 β‘β f2 -> Pair s t `α΅₯β f1 = Pair s t `α΅₯β f2
forall (Ξ : t_ctx) (A : pre_ty) (u : term Ξ β A),
(forall (Ξ : t_ctx) (f1f2 : Ξ =[ val ]> Ξ),
f1 β‘β f2 -> u `ββ f1 = u `ββ f2) ->
forallv : term Ξ Β¬ A,
(forall (Ξ : t_ctx) (f1f2 : Ξ =[ val ]> Ξ),
f1 β‘β f2 -> v `ββ f1 = v `ββ f2) ->
forall (Ξ : t_ctx) (f1f2 : Ξ =[ val ]> Ξ),
f1 β‘β f2 -> Cut u v ββ f1 = Cut u v ββ f2
Ξ: t_ctx A: pre_ty s: state (Ξ βΆβ Β¬ A) H: forall (Ξ : t_ctx)
(f1f2 : (Ξ βΆβ Β¬ A) =[ val ]> Ξ),
f1 β‘β f2 -> s ββ f1 = s ββ f2 Ξ: t_ctx f1, f2: Ξ =[ val ]> Ξ H0: f1 β‘β f2
s_subst (Ξ βΆβ Β¬ A) s (Ξ βΆβ Β¬ A) (a_shift1 f1) =
s_subst (Ξ βΆβ Β¬ A) s (Ξ βΆβ Β¬ A) (a_shift1 f2)
Ξ: t_ctx A: pre_ty v: whn Ξ A H: forall (Ξ : t_ctx) (f1f2 : Ξ =[ val ]> Ξ),
f1 β‘β f2 -> v `α΅₯β f1 = v `α΅₯β f2 Ξ: t_ctx f1, f2: Ξ =[ val ]> Ξ H0: f1 β‘β f2
v `α΅₯β f1 = v `α΅₯β f2
Ξ: t_ctx A: pre_ty s: state (Ξ βΆβ β A) H: forall (Ξ : t_ctx)
(f1f2 : (Ξ βΆβ β A) =[ val ]> Ξ),
f1 β‘β f2 -> s ββ f1 = s ββ f2 Ξ: t_ctx f1, f2: Ξ =[ val ]> Ξ H0: f1 β‘β f2
s_subst (Ξ βΆβ β A) s (Ξ βΆβ β A) (a_shift1 f1) =
s_subst (Ξ βΆβ β A) s (Ξ βΆβ β A) (a_shift1 f2)
Ξ: t_ctx A, B: pre_ty v: whn Ξ A H: forall (Ξ : t_ctx) (f1f2 : Ξ =[ val ]> Ξ),
f1 β‘β f2 -> v `α΅₯β f1 = v `α΅₯β f2 k: term Ξ Β¬ B H0: forall (Ξ : t_ctx) (f1f2 : Ξ =[ val ]> Ξ),
f1 β‘β f2 -> k `ββ f1 = k `ββ f2 Ξ: t_ctx f1, f2: Ξ =[ val ]> Ξ H1: f1 β‘β f2
v `α΅₯β f1 = v `α΅₯β f2
Ξ: t_ctx A, B: pre_ty v: whn Ξ A H: forall (Ξ : t_ctx) (f1f2 : Ξ =[ val ]> Ξ),
f1 β‘β f2 -> v `α΅₯β f1 = v `α΅₯β f2 k: term Ξ Β¬ B H0: forall (Ξ : t_ctx) (f1f2 : Ξ =[ val ]> Ξ),
f1 β‘β f2 -> k `ββ f1 = k `ββ f2 Ξ: t_ctx f1, f2: Ξ =[ val ]> Ξ H1: f1 β‘β f2
k `ββ f1 = k `ββ f2
Ξ: t_ctx A, B: pre_ty k: term Ξ Β¬ A H: forall (Ξ : t_ctx) (f1f2 : Ξ =[ val ]> Ξ),
f1 β‘β f2 -> k `ββ f1 = k `ββ f2 Ξ: t_ctx f1, f2: Ξ =[ val ]> Ξ H0: f1 β‘β f2
k `ββ f1 = k `ββ f2
Ξ: t_ctx A, B: pre_ty k: term Ξ Β¬ B H: forall (Ξ : t_ctx) (f1f2 : Ξ =[ val ]> Ξ),
f1 β‘β f2 -> k `ββ f1 = k `ββ f2 Ξ: t_ctx f1, f2: Ξ =[ val ]> Ξ H0: f1 β‘β f2
k `ββ f1 = k `ββ f2
Ξ: t_ctx A, B: pre_ty s: state (Ξ βΆβ β A) H: forall (Ξ : t_ctx)
(f1f2 : (Ξ βΆβ β A) =[ val ]> Ξ),
f1 β‘β f2 -> s ββ f1 = s ββ f2 t: state (Ξ βΆβ β B) H0: forall (Ξ : t_ctx)
(f1f2 : (Ξ βΆβ β B) =[ val ]> Ξ),
f1 β‘β f2 -> t ββ f1 = t ββ f2 Ξ: t_ctx f1, f2: Ξ =[ val ]> Ξ H1: f1 β‘β f2
s_subst (Ξ βΆβ β A) s (Ξ βΆβ β A) (a_shift1 f1) =
s_subst (Ξ βΆβ β A) s (Ξ βΆβ β A) (a_shift1 f2)
Ξ: t_ctx A, B: pre_ty s: state (Ξ βΆβ β A) H: forall (Ξ : t_ctx)
(f1f2 : (Ξ βΆβ β A) =[ val ]> Ξ),
f1 β‘β f2 -> s ββ f1 = s ββ f2 t: state (Ξ βΆβ β B) H0: forall (Ξ : t_ctx)
(f1f2 : (Ξ βΆβ β B) =[ val ]> Ξ),
f1 β‘β f2 -> t ββ f1 = t ββ f2 Ξ: t_ctx f1, f2: Ξ =[ val ]> Ξ H1: f1 β‘β f2
s_subst (Ξ βΆβ β B) t (Ξ βΆβ β B) (a_shift1 f1) =
s_subst (Ξ βΆβ β B) t (Ξ βΆβ β B) (a_shift1 f2)
Ξ: t_ctx A, B: pre_ty v: whn Ξ A H: forall (Ξ : t_ctx) (f1f2 : Ξ =[ val ]> Ξ),
f1 β‘β f2 -> v `α΅₯β f1 = v `α΅₯β f2 Ξ: t_ctx f1, f2: Ξ =[ val ]> Ξ H0: f1 β‘β f2
v `α΅₯β f1 = v `α΅₯β f2
Ξ: t_ctx A, B: pre_ty v: whn Ξ B H: forall (Ξ : t_ctx) (f1f2 : Ξ =[ val ]> Ξ),
f1 β‘β f2 -> v `α΅₯β f1 = v `α΅₯β f2 Ξ: t_ctx f1, f2: Ξ =[ val ]> Ξ H0: f1 β‘β f2
v `α΅₯β f1 = v `α΅₯β f2
Ξ: t_ctx A, B: pre_ty s: state (Ξ βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B) H: forall (Ξ : t_ctx)
(f1f2 : (Ξ βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B) =[ val
]> Ξ), f1 β‘β f2 -> s ββ f1 = s ββ f2 Ξ: t_ctx f1, f2: Ξ =[ val ]> Ξ H0: f1 β‘β f2
s_subst (Ξ βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B) s
(Ξ βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B) (a_shift3 f1) =
s_subst (Ξ βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B) s
(Ξ βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B) (a_shift3 f2)
Ξ: t_ctx A, B: pre_ty s: state (Ξ βΆβ Β¬ A) H: forall (Ξ : t_ctx)
(f1f2 : (Ξ βΆβ Β¬ A) =[ val ]> Ξ),
f1 β‘β f2 -> s ββ f1 = s ββ f2 t: state (Ξ βΆβ Β¬ B) H0: forall (Ξ : t_ctx)
(f1f2 : (Ξ βΆβ Β¬ B) =[ val ]> Ξ),
f1 β‘β f2 -> t ββ f1 = t ββ f2 Ξ: t_ctx f1, f2: Ξ =[ val ]> Ξ H1: f1 β‘β f2
s_subst (Ξ βΆβ Β¬ A) s (Ξ βΆβ Β¬ A) (a_shift1 f1) =
s_subst (Ξ βΆβ Β¬ A) s (Ξ βΆβ Β¬ A) (a_shift1 f2)
Ξ: t_ctx A, B: pre_ty s: state (Ξ βΆβ Β¬ A) H: forall (Ξ : t_ctx)
(f1f2 : (Ξ βΆβ Β¬ A) =[ val ]> Ξ),
f1 β‘β f2 -> s ββ f1 = s ββ f2 t: state (Ξ βΆβ Β¬ B) H0: forall (Ξ : t_ctx)
(f1f2 : (Ξ βΆβ Β¬ B) =[ val ]> Ξ),
f1 β‘β f2 -> t ββ f1 = t ββ f2 Ξ: t_ctx f1, f2: Ξ =[ val ]> Ξ H1: f1 β‘β f2
s_subst (Ξ βΆβ Β¬ B) t (Ξ βΆβ Β¬ B) (a_shift1 f1) =
s_subst (Ξ βΆβ Β¬ B) t (Ξ βΆβ Β¬ B) (a_shift1 f2)
Ξ: t_ctx A: pre_ty u: term Ξ β A H: forall (Ξ : t_ctx) (f1f2 : Ξ =[ val ]> Ξ),
f1 β‘β f2 -> u `ββ f1 = u `ββ f2 v: term Ξ Β¬ A H0: forall (Ξ : t_ctx) (f1f2 : Ξ =[ val ]> Ξ),
f1 β‘β f2 -> v `ββ f1 = v `ββ f2 Ξ: t_ctx f1, f2: Ξ =[ val ]> Ξ H1: f1 β‘β f2
u `ββ f1 = u `ββ f2
Ξ: t_ctx A: pre_ty u: term Ξ β A H: forall (Ξ : t_ctx) (f1f2 : Ξ =[ val ]> Ξ),
f1 β‘β f2 -> u `ββ f1 = u `ββ f2 v: term Ξ Β¬ A H0: forall (Ξ : t_ctx) (f1f2 : Ξ =[ val ]> Ξ),
f1 β‘β f2 -> v `ββ f1 = v `ββ f2 Ξ: t_ctx f1, f2: Ξ =[ val ]> Ξ H1: f1 β‘β f2
v `ββ f1 = v `ββ f2
Ξ: t_ctx A: pre_ty s: state (Ξ βΆβ Β¬ A) H: forall (Ξ : t_ctx)
(f1f2 : (Ξ βΆβ Β¬ A) =[ val ]> Ξ),
f1 β‘β f2 -> s ββ f1 = s ββ f2 Ξ: t_ctx f1, f2: Ξ =[ val ]> Ξ H0: f1 β‘β f2
a_shift1 f1 β‘β a_shift1 f2
Ξ: t_ctx A: pre_ty s: state (Ξ βΆβ β A) H: forall (Ξ : t_ctx)
(f1f2 : (Ξ βΆβ β A) =[ val ]> Ξ),
f1 β‘β f2 -> s ββ f1 = s ββ f2 Ξ: t_ctx f1, f2: Ξ =[ val ]> Ξ H0: f1 β‘β f2
a_shift1 f1 β‘β a_shift1 f2
Ξ: t_ctx A, B: pre_ty s: state (Ξ βΆβ β A) H: forall (Ξ : t_ctx)
(f1f2 : (Ξ βΆβ β A) =[ val ]> Ξ),
f1 β‘β f2 -> s ββ f1 = s ββ f2 t: state (Ξ βΆβ β B) H0: forall (Ξ : t_ctx)
(f1f2 : (Ξ βΆβ β B) =[ val ]> Ξ),
f1 β‘β f2 -> t ββ f1 = t ββ f2 Ξ: t_ctx f1, f2: Ξ =[ val ]> Ξ H1: f1 β‘β f2
a_shift1 f1 β‘β a_shift1 f2
Ξ: t_ctx A, B: pre_ty s: state (Ξ βΆβ β A) H: forall (Ξ : t_ctx)
(f1f2 : (Ξ βΆβ β A) =[ val ]> Ξ),
f1 β‘β f2 -> s ββ f1 = s ββ f2 t: state (Ξ βΆβ β B) H0: forall (Ξ : t_ctx)
(f1f2 : (Ξ βΆβ β B) =[ val ]> Ξ),
f1 β‘β f2 -> t ββ f1 = t ββ f2 Ξ: t_ctx f1, f2: Ξ =[ val ]> Ξ H1: f1 β‘β f2
a_shift1 f1 β‘β a_shift1 f2
Ξ: t_ctx A, B: pre_ty s: state (Ξ βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B) H: forall (Ξ : t_ctx)
(f1f2 : (Ξ βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B) =[ val
]> Ξ), f1 β‘β f2 -> s ββ f1 = s ββ f2 Ξ: t_ctx f1, f2: Ξ =[ val ]> Ξ H0: f1 β‘β f2
a_shift3 f1 β‘β a_shift3 f2
Ξ: t_ctx A, B: pre_ty s: state (Ξ βΆβ Β¬ A) H: forall (Ξ : t_ctx)
(f1f2 : (Ξ βΆβ Β¬ A) =[ val ]> Ξ),
f1 β‘β f2 -> s ββ f1 = s ββ f2 t: state (Ξ βΆβ Β¬ B) H0: forall (Ξ : t_ctx)
(f1f2 : (Ξ βΆβ Β¬ B) =[ val ]> Ξ),
f1 β‘β f2 -> t ββ f1 = t ββ f2 Ξ: t_ctx f1, f2: Ξ =[ val ]> Ξ H1: f1 β‘β f2
a_shift1 f1 β‘β a_shift1 f2
Ξ: t_ctx A, B: pre_ty s: state (Ξ βΆβ Β¬ A) H: forall (Ξ : t_ctx)
(f1f2 : (Ξ βΆβ Β¬ A) =[ val ]> Ξ),
f1 β‘β f2 -> s ββ f1 = s ββ f2 t: state (Ξ βΆβ Β¬ B) H0: forall (Ξ : t_ctx)
(f1f2 : (Ξ βΆβ Β¬ B) =[ val ]> Ξ),
f1 β‘β f2 -> t ββ f1 = t ββ f2 Ξ: t_ctx f1, f2: Ξ =[ val ]> Ξ H1: f1 β‘β f2
a_shift1 f1 β‘β a_shift1 f2
all: first [ apply a_shift1_eq | apply a_shift3_eq ]; auto.Qed.
Ξ: t_ctx a: ty t: term Ξ a Ξ: t_ctx
Proper (asgn_eq Ξ Ξ ==> eq) (t_subst Ξ a t Ξ)
intros f1 f2 H1; nowapply (term_ind_mut _ _ _ sub_proper_prf).Qed.
Ξ: t_ctx a: pre_ty v: whn Ξ a Ξ: t_ctx
Proper (asgn_eq Ξ Ξ ==> eq) (w_subst Ξ a v Ξ)
intros f1 f2 H1; nowapply (whn_ind_mut _ _ _ sub_proper_prf).Qed.
Ξ: t_ctx s: state Ξ Ξ: t_ctx
Proper (asgn_eq Ξ Ξ ==> eq) (s_subst Ξ s Ξ)
intros f1 f2 H1; nowapply (state_ind_mut _ _ _ sub_proper_prf).Qed.
Ξ: t_ctx a: ty v: val Ξ a Ξ: t_ctx
Proper (asgn_eq Ξ Ξ ==> eq) (v_subst Ξ a v Ξ)
Ξ: t_ctx p: pre_ty v: val Ξ β p Ξ: t_ctx
Proper (asgn_eq Ξ Ξ ==> eq) (v_subst Ξ β p v Ξ)
Ξ: t_ctx p: pre_ty v: val Ξ Β¬ p Ξ: t_ctx
Proper (asgn_eq Ξ Ξ ==> eq) (v_subst Ξ Β¬ p v Ξ)
Ξ: t_ctx p: pre_ty v: val Ξ β p Ξ: t_ctx
Proper (asgn_eq Ξ Ξ ==> eq) (v_subst Ξ β p v Ξ)
nowapply w_sub_eq.
Ξ: t_ctx p: pre_ty v: val Ξ Β¬ p Ξ: t_ctx
Proper (asgn_eq Ξ Ξ ==> eq) (v_subst Ξ Β¬ p v Ξ)
intros ? ? H1 ? ? H2 ? ?; cbn; rewrite H1; noweapply v_sub_eq.Qed.Definitiont_ren_sub_PΞ1A (t : term Ξ1 A) : Prop :=
forallΞ2Ξ3 (f1 : Ξ1 =[val]> Ξ2) (f2 : Ξ2 β Ξ3),
(t `ββ f1) ββα΅£ f2 = t `ββ (f1 βα΅£ f2) .Definitionw_ren_sub_PΞ1A (v : whn Ξ1 A) : Prop :=
forallΞ2Ξ3 (f1 : Ξ1 =[val]> Ξ2) (f2 : Ξ2 β Ξ3),
(v `α΅₯β f1) `α΅₯βα΅£ f2 = v `α΅₯β (f1 βα΅£ f2) .Definitions_ren_sub_PΞ1 (s : state Ξ1) : Prop :=
forallΞ2Ξ3 (f1 : Ξ1 =[val]> Ξ2) (f2 : Ξ2 β Ξ3),
(s ββ f1) ββα΅£ f2 = s ββ (f1 βα΅£ f2) .
syn_ind_args t_ren_sub_P w_ren_sub_P s_ren_sub_P
forall (Ξ : t_ctx) (A : pre_ty) (s : state (Ξ βΆβ Β¬ A)),
s_ren_sub_P (Ξ βΆβ Β¬ A) s -> t_ren_sub_P Ξ β A (Mu s)
forall (Ξ : t_ctx) (A : pre_ty) (v : whn Ξ A),
w_ren_sub_P Ξ A v -> t_ren_sub_P Ξ β A (Val v)
forall (Ξ : t_ctx) (A : pre_ty) (i : Ξ β Β¬ A),
t_ren_sub_P Ξ Β¬ A (VarR i)
forall (Ξ : t_ctx) (A : pre_ty) (s : state (Ξ βΆβ β A)),
s_ren_sub_P (Ξ βΆβ β A) s -> t_ren_sub_P Ξ Β¬ A (MuT s)
forallΞ : t_ctx, t_ren_sub_P Ξ Β¬ `0 Boom
forall (Ξ : t_ctx) (AB : pre_ty) (v : whn Ξ A),
w_ren_sub_P Ξ A v ->
forallk : term Ξ Β¬ B,
t_ren_sub_P Ξ Β¬ B k ->
t_ren_sub_P Ξ Β¬ (A `β B) (App v k)
forall (Ξ : t_ctx) (AB : pre_ty) (k : term Ξ Β¬ A),
t_ren_sub_P Ξ Β¬ A k ->
t_ren_sub_P Ξ Β¬ (A `Γ B) (Fst k)
forall (Ξ : t_ctx) (AB : pre_ty) (k : term Ξ Β¬ B),
t_ren_sub_P Ξ Β¬ B k ->
t_ren_sub_P Ξ Β¬ (A `Γ B) (Snd k)
forall (Ξ : t_ctx) (AB : pre_ty)
(s : state (Ξ βΆβ β A)),
s_ren_sub_P (Ξ βΆβ β A) s ->
forallt : state (Ξ βΆβ β B),
s_ren_sub_P (Ξ βΆβ β B) t ->
t_ren_sub_P Ξ Β¬ (A `+ B) (Case s t)
forall (Ξ : t_ctx) (A : pre_ty) (i : Ξ β β A),
w_ren_sub_P Ξ A (VarL i)
forall (Ξ : t_ctx) (AB : pre_ty) (v : whn Ξ A),
w_ren_sub_P Ξ A v -> w_ren_sub_P Ξ (A `+ B) (Inl v)
forall (Ξ : t_ctx) (AB : pre_ty) (v : whn Ξ B),
w_ren_sub_P Ξ B v -> w_ren_sub_P Ξ (A `+ B) (Inr v)
forallΞ : t_ctx, w_ren_sub_P Ξ `1 Tt
forall (Ξ : t_ctx) (AB : pre_ty)
(s : state (Ξ βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B)),
s_ren_sub_P (Ξ βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B) s ->
w_ren_sub_P Ξ (A `β B) (Lam s)
forall (Ξ : t_ctx) (AB : pre_ty)
(s : state (Ξ βΆβ Β¬ A)),
s_ren_sub_P (Ξ βΆβ Β¬ A) s ->
forallt : state (Ξ βΆβ Β¬ B),
s_ren_sub_P (Ξ βΆβ Β¬ B) t ->
w_ren_sub_P Ξ (A `Γ B) (Pair s t)
forall (Ξ : t_ctx) (A : pre_ty) (u : term Ξ β A),
t_ren_sub_P Ξ β A u ->
forallv : term Ξ Β¬ A,
t_ren_sub_P Ξ Β¬ A v -> s_ren_sub_P Ξ (Cut u v)
forall (Ξ : t_ctx) (A : pre_ty) (s : state (Ξ βΆβ Β¬ A)),
(forall (Ξ2Ξ3 : t_ctx) (f1 : (Ξ βΆβ Β¬ A) =[ val ]> Ξ2)
(f2 : Ξ2 β Ξ3), (s ββ f1) ββα΅£ f2 = s ββ f1 βα΅£ f2) ->
forall (Ξ2Ξ3 : t_ctx) (f1 : Ξ =[ val ]> Ξ2)
(f2 : Ξ2 β Ξ3),
(Mu s `ββ f1) ββα΅£ f2 = Mu s `ββ f1 βα΅£ f2
forall (Ξ : t_ctx) (A : pre_ty) (v : whn Ξ A),
(forall (Ξ2Ξ3 : t_ctx) (f1 : Ξ =[ val ]> Ξ2)
(f2 : Ξ2 β Ξ3), (v `α΅₯β f1) `α΅₯βα΅£ f2 = v `α΅₯β f1 βα΅£ f2) ->
forall (Ξ2Ξ3 : t_ctx) (f1 : Ξ =[ val ]> Ξ2)
(f2 : Ξ2 β Ξ3),
(Val v `ββ f1) ββα΅£ f2 = Val v `ββ f1 βα΅£ f2
forall (Ξ : t_ctx) (A : pre_ty) (i : Ξ β Β¬ A)
(Ξ2Ξ3 : t_ctx) (f1 : Ξ =[ val ]> Ξ2) (f2 : Ξ2 β Ξ3),
(VarR i `ββ f1) ββα΅£ f2 = VarR i `ββ f1 βα΅£ f2
forall (Ξ : t_ctx) (A : pre_ty) (s : state (Ξ βΆβ β A)),
(forall (Ξ2Ξ3 : t_ctx) (f1 : (Ξ βΆβ β A) =[ val ]> Ξ2)
(f2 : Ξ2 β Ξ3), (s ββ f1) ββα΅£ f2 = s ββ f1 βα΅£ f2) ->
forall (Ξ2Ξ3 : t_ctx) (f1 : Ξ =[ val ]> Ξ2)
(f2 : Ξ2 β Ξ3),
(MuT s `ββ f1) ββα΅£ f2 = MuT s `ββ f1 βα΅£ f2
forall (Ξ : t_ctx) (AB : pre_ty)
(s : state (Ξ βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B)),
(forall (Ξ2Ξ3 : t_ctx)
(f1 : (Ξ βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B) =[ val ]> Ξ2)
(f2 : Ξ2 β Ξ3), (s ββ f1) ββα΅£ f2 = s ββ f1 βα΅£ f2) ->
forall (Ξ2Ξ3 : t_ctx) (f1 : Ξ =[ val ]> Ξ2)
(f2 : Ξ2 β Ξ3),
(Lam s `α΅₯β f1) `α΅₯βα΅£ f2 = Lam s `α΅₯β f1 βα΅£ f2
forall (Ξ : t_ctx) (AB : pre_ty)
(s : state (Ξ βΆβ Β¬ A)),
(forall (Ξ2Ξ3 : t_ctx) (f1 : (Ξ βΆβ Β¬ A) =[ val ]> Ξ2)
(f2 : Ξ2 β Ξ3), (s ββ f1) ββα΅£ f2 = s ββ f1 βα΅£ f2) ->
forallt : state (Ξ βΆβ Β¬ B),
(forall (Ξ2Ξ3 : t_ctx) (f1 : (Ξ βΆβ Β¬ B) =[ val ]> Ξ2)
(f2 : Ξ2 β Ξ3), (t ββ f1) ββα΅£ f2 = t ββ f1 βα΅£ f2) ->
forall (Ξ2Ξ3 : t_ctx) (f1 : Ξ =[ val ]> Ξ2)
(f2 : Ξ2 β Ξ3),
(Pair s t `α΅₯β f1) `α΅₯βα΅£ f2 = Pair s t `α΅₯β f1 βα΅£ f2
forall (Ξ : t_ctx) (A : pre_ty) (u : term Ξ β A),
(forall (Ξ2Ξ3 : t_ctx) (f1 : Ξ =[ val ]> Ξ2)
(f2 : Ξ2 β Ξ3), (u `ββ f1) ββα΅£ f2 = u `ββ f1 βα΅£ f2) ->
forallv : term Ξ Β¬ A,
(forall (Ξ2Ξ3 : t_ctx) (f1 : Ξ =[ val ]> Ξ2)
(f2 : Ξ2 β Ξ3), (v `ββ f1) ββα΅£ f2 = v `ββ f1 βα΅£ f2) ->
forall (Ξ2Ξ3 : t_ctx) (f1 : Ξ =[ val ]> Ξ2)
(f2 : Ξ2 β Ξ3),
(Cut u v ββ f1) ββα΅£ f2 = Cut u v ββ f1 βα΅£ f2
Ξ: t_ctx A: pre_ty s: state (Ξ βΆβ Β¬ A) H: forall (Ξ2Ξ3 : t_ctx)
(f1 : (Ξ βΆβ Β¬ A) =[ val ]> Ξ2) (f2 : Ξ2 β Ξ3),
(s ββ f1) ββα΅£ f2 = s ββ f1 βα΅£ f2 Ξ2, Ξ3: t_ctx f1: Ξ =[ val ]> Ξ2 f2: Ξ2 β Ξ3
s_subst (Ξ βΆβ Β¬ A) s (Ξ2 βΆβ Β¬ A) (a_shift1 f1)
ββα΅£ r_shift1 f2 =
s_subst (Ξ βΆβ Β¬ A) s (Ξ3 βΆβ Β¬ A) (a_shift1 (f1 βα΅£ f2))
Ξ: t_ctx A: pre_ty s: state (Ξ βΆβ β A) H: forall (Ξ2Ξ3 : t_ctx)
(f1 : (Ξ βΆβ β A) =[ val ]> Ξ2) (f2 : Ξ2 β Ξ3),
(s ββ f1) ββα΅£ f2 = s ββ f1 βα΅£ f2 Ξ2, Ξ3: t_ctx f1: Ξ =[ val ]> Ξ2 f2: Ξ2 β Ξ3
s_subst (Ξ βΆβ β A) s (Ξ2 βΆβ β A) (a_shift1 f1)
ββα΅£ r_shift1 f2 =
s_subst (Ξ βΆβ β A) s (Ξ3 βΆβ β A) (a_shift1 (f1 βα΅£ f2))
Ξ: t_ctx A, B: pre_ty s: state (Ξ βΆβ β A) H: forall (Ξ2Ξ3 : t_ctx)
(f1 : (Ξ βΆβ β A) =[ val ]> Ξ2) (f2 : Ξ2 β Ξ3),
(s ββ f1) ββα΅£ f2 = s ββ f1 βα΅£ f2 t: state (Ξ βΆβ β B) H0: forall (Ξ2Ξ3 : t_ctx)
(f1 : (Ξ βΆβ β B) =[ val ]> Ξ2) (f2 : Ξ2 β Ξ3),
(t ββ f1) ββα΅£ f2 = t ββ f1 βα΅£ f2 Ξ2, Ξ3: t_ctx f1: Ξ =[ val ]> Ξ2 f2: Ξ2 β Ξ3
s_subst (Ξ βΆβ β A) s (Ξ2 βΆβ β A) (a_shift1 f1)
ββα΅£ r_shift1 f2 =
s_subst (Ξ βΆβ β A) s (Ξ3 βΆβ β A) (a_shift1 (f1 βα΅£ f2))
Ξ: t_ctx A, B: pre_ty s: state (Ξ βΆβ β A) H: forall (Ξ2Ξ3 : t_ctx)
(f1 : (Ξ βΆβ β A) =[ val ]> Ξ2) (f2 : Ξ2 β Ξ3),
(s ββ f1) ββα΅£ f2 = s ββ f1 βα΅£ f2 t: state (Ξ βΆβ β B) H0: forall (Ξ2Ξ3 : t_ctx)
(f1 : (Ξ βΆβ β B) =[ val ]> Ξ2) (f2 : Ξ2 β Ξ3),
(t ββ f1) ββα΅£ f2 = t ββ f1 βα΅£ f2 Ξ2, Ξ3: t_ctx f1: Ξ =[ val ]> Ξ2 f2: Ξ2 β Ξ3
s_subst (Ξ βΆβ β B) t (Ξ2 βΆβ β B) (a_shift1 f1)
ββα΅£ r_shift1 f2 =
s_subst (Ξ βΆβ β B) t (Ξ3 βΆβ β B) (a_shift1 (f1 βα΅£ f2))
Ξ: t_ctx A, B: pre_ty s: state (Ξ βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B) H: forall (Ξ2Ξ3 : t_ctx)
(f1 : (Ξ βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B) =[ val
]> Ξ2) (f2 : Ξ2 β Ξ3),
(s ββ f1) ββα΅£ f2 = s ββ f1 βα΅£ f2 Ξ2, Ξ3: t_ctx f1: Ξ =[ val ]> Ξ2 f2: Ξ2 β Ξ3
s_subst (Ξ βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B) s
(Ξ2 βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B) (a_shift3 f1)
ββα΅£ r_shift3 f2 =
s_subst (Ξ βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B) s
(Ξ3 βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B)
(a_shift3 (f1 βα΅£ f2))
Ξ: t_ctx A, B: pre_ty s: state (Ξ βΆβ Β¬ A) H: forall (Ξ2Ξ3 : t_ctx)
(f1 : (Ξ βΆβ Β¬ A) =[ val ]> Ξ2) (f2 : Ξ2 β Ξ3),
(s ββ f1) ββα΅£ f2 = s ββ f1 βα΅£ f2 t: state (Ξ βΆβ Β¬ B) H0: forall (Ξ2Ξ3 : t_ctx)
(f1 : (Ξ βΆβ Β¬ B) =[ val ]> Ξ2) (f2 : Ξ2 β Ξ3),
(t ββ f1) ββα΅£ f2 = t ββ f1 βα΅£ f2 Ξ2, Ξ3: t_ctx f1: Ξ =[ val ]> Ξ2 f2: Ξ2 β Ξ3
s_subst (Ξ βΆβ Β¬ A) s (Ξ2 βΆβ Β¬ A) (a_shift1 f1)
ββα΅£ r_shift1 f2 =
s_subst (Ξ βΆβ Β¬ A) s (Ξ3 βΆβ Β¬ A) (a_shift1 (f1 βα΅£ f2))
Ξ: t_ctx A, B: pre_ty s: state (Ξ βΆβ Β¬ A) H: forall (Ξ2Ξ3 : t_ctx)
(f1 : (Ξ βΆβ Β¬ A) =[ val ]> Ξ2) (f2 : Ξ2 β Ξ3),
(s ββ f1) ββα΅£ f2 = s ββ f1 βα΅£ f2 t: state (Ξ βΆβ Β¬ B) H0: forall (Ξ2Ξ3 : t_ctx)
(f1 : (Ξ βΆβ Β¬ B) =[ val ]> Ξ2) (f2 : Ξ2 β Ξ3),
(t ββ f1) ββα΅£ f2 = t ββ f1 βα΅£ f2 Ξ2, Ξ3: t_ctx f1: Ξ =[ val ]> Ξ2 f2: Ξ2 β Ξ3
s_subst (Ξ βΆβ Β¬ B) t (Ξ2 βΆβ Β¬ B) (a_shift1 f1)
ββα΅£ r_shift1 f2 =
s_subst (Ξ βΆβ Β¬ B) t (Ξ3 βΆβ Β¬ B) (a_shift1 (f1 βα΅£ f2))
all: first [ rewrite a_shift1_ren_r | rewrite a_shift3_ren_r ]; auto.Qed.
Ξ1, Ξ2, Ξ3: t_ctx f1: Ξ1 =[ val ]> Ξ2 f2: Ξ2 β Ξ3 A: ty t: term Ξ1 A
(t `ββ f1) ββα΅£ f2 = t `ββ f1 βα΅£ f2
nowapply (term_ind_mut _ _ _ ren_sub_prf).Qed.
Ξ1, Ξ2, Ξ3: t_ctx f1: Ξ1 =[ val ]> Ξ2 f2: Ξ2 β Ξ3 A: pre_ty v: whn Ξ1 A
(v `α΅₯β f1) `α΅₯βα΅£ f2 = v `α΅₯β f1 βα΅£ f2
nowapply (whn_ind_mut _ _ _ ren_sub_prf).Qed.
Ξ1, Ξ2, Ξ3: t_ctx f1: Ξ1 =[ val ]> Ξ2 f2: Ξ2 β Ξ3 s: state Ξ1
(s ββ f1) ββα΅£ f2 = s ββ f1 βα΅£ f2
nowapply (state_ind_mut _ _ _ ren_sub_prf).Qed.
Ξ1, Ξ2, Ξ3: t_ctx f1: Ξ1 =[ val ]> Ξ2 f2: Ξ2 β Ξ3 A: ty v: val Ξ1 A
(v α΅₯β f1) α΅₯βα΅£ f2 = v α΅₯β f1 βα΅£ f2
Ξ1, Ξ2, Ξ3: t_ctx f1: Ξ1 =[ val ]> Ξ2 f2: Ξ2 β Ξ3 p: pre_ty v: val Ξ1 β p
(v α΅₯β f1) α΅₯βα΅£ f2 = v α΅₯β f1 βα΅£ f2
Ξ1, Ξ2, Ξ3: t_ctx f1: Ξ1 =[ val ]> Ξ2 f2: Ξ2 β Ξ3 p: pre_ty v: val Ξ1 Β¬ p
(v α΅₯β f1) α΅₯βα΅£ f2 = v α΅₯β f1 βα΅£ f2
Ξ1, Ξ2, Ξ3: t_ctx f1: Ξ1 =[ val ]> Ξ2 f2: Ξ2 β Ξ3 p: pre_ty v: val Ξ1 β p
(v α΅₯β f1) α΅₯βα΅£ f2 = v α΅₯β f1 βα΅£ f2
nowapply w_ren_sub.
Ξ1, Ξ2, Ξ3: t_ctx f1: Ξ1 =[ val ]> Ξ2 f2: Ξ2 β Ξ3 p: pre_ty v: val Ξ1 Β¬ p
(v α΅₯β f1) α΅₯βα΅£ f2 = v α΅₯β f1 βα΅£ f2
nowapply t_ren_sub.Qed.Definitiont_sub_ren_PΞ1A (t : term Ξ1 A) : Prop :=
forallΞ2Ξ3 (f1 : Ξ1 β Ξ2) (f2 : Ξ2 =[val]> Ξ3),
(t ββα΅£ f1) `ββ f2 = t `ββ (f1 α΅£β f2).Definitionw_sub_ren_PΞ1A (v : whn Ξ1 A) : Prop :=
forallΞ2Ξ3 (f1 : Ξ1 β Ξ2) (f2 : Ξ2 =[val]> Ξ3),
(v `α΅₯βα΅£ f1) `α΅₯β f2 = v `α΅₯β (f1 α΅£β f2).Definitions_sub_ren_PΞ1 (s : state Ξ1) : Prop :=
forallΞ2Ξ3 (f1 : Ξ1 β Ξ2) (f2 : Ξ2 =[val]> Ξ3),
(s ββα΅£ f1) ββ f2 = s ββ (f1 α΅£β f2).
syn_ind_args t_sub_ren_P w_sub_ren_P s_sub_ren_P
forall (Ξ : t_ctx) (A : pre_ty) (s : state (Ξ βΆβ Β¬ A)),
s_sub_ren_P (Ξ βΆβ Β¬ A) s -> t_sub_ren_P Ξ β A (Mu s)
forall (Ξ : t_ctx) (A : pre_ty) (v : whn Ξ A),
w_sub_ren_P Ξ A v -> t_sub_ren_P Ξ β A (Val v)
forall (Ξ : t_ctx) (A : pre_ty) (i : Ξ β Β¬ A),
t_sub_ren_P Ξ Β¬ A (VarR i)
forall (Ξ : t_ctx) (A : pre_ty) (s : state (Ξ βΆβ β A)),
s_sub_ren_P (Ξ βΆβ β A) s -> t_sub_ren_P Ξ Β¬ A (MuT s)
forallΞ : t_ctx, t_sub_ren_P Ξ Β¬ `0 Boom
forall (Ξ : t_ctx) (AB : pre_ty) (v : whn Ξ A),
w_sub_ren_P Ξ A v ->
forallk : term Ξ Β¬ B,
t_sub_ren_P Ξ Β¬ B k ->
t_sub_ren_P Ξ Β¬ (A `β B) (App v k)
forall (Ξ : t_ctx) (AB : pre_ty) (k : term Ξ Β¬ A),
t_sub_ren_P Ξ Β¬ A k ->
t_sub_ren_P Ξ Β¬ (A `Γ B) (Fst k)
forall (Ξ : t_ctx) (AB : pre_ty) (k : term Ξ Β¬ B),
t_sub_ren_P Ξ Β¬ B k ->
t_sub_ren_P Ξ Β¬ (A `Γ B) (Snd k)
forall (Ξ : t_ctx) (AB : pre_ty)
(s : state (Ξ βΆβ β A)),
s_sub_ren_P (Ξ βΆβ β A) s ->
forallt : state (Ξ βΆβ β B),
s_sub_ren_P (Ξ βΆβ β B) t ->
t_sub_ren_P Ξ Β¬ (A `+ B) (Case s t)
forall (Ξ : t_ctx) (A : pre_ty) (i : Ξ β β A),
w_sub_ren_P Ξ A (VarL i)
forall (Ξ : t_ctx) (AB : pre_ty) (v : whn Ξ A),
w_sub_ren_P Ξ A v -> w_sub_ren_P Ξ (A `+ B) (Inl v)
forall (Ξ : t_ctx) (AB : pre_ty) (v : whn Ξ B),
w_sub_ren_P Ξ B v -> w_sub_ren_P Ξ (A `+ B) (Inr v)
forallΞ : t_ctx, w_sub_ren_P Ξ `1 Tt
forall (Ξ : t_ctx) (AB : pre_ty)
(s : state (Ξ βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B)),
s_sub_ren_P (Ξ βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B) s ->
w_sub_ren_P Ξ (A `β B) (Lam s)
forall (Ξ : t_ctx) (AB : pre_ty)
(s : state (Ξ βΆβ Β¬ A)),
s_sub_ren_P (Ξ βΆβ Β¬ A) s ->
forallt : state (Ξ βΆβ Β¬ B),
s_sub_ren_P (Ξ βΆβ Β¬ B) t ->
w_sub_ren_P Ξ (A `Γ B) (Pair s t)
forall (Ξ : t_ctx) (A : pre_ty) (u : term Ξ β A),
t_sub_ren_P Ξ β A u ->
forallv : term Ξ Β¬ A,
t_sub_ren_P Ξ Β¬ A v -> s_sub_ren_P Ξ (Cut u v)
forall (Ξ : t_ctx) (A : pre_ty) (s : state (Ξ βΆβ Β¬ A)),
(forall (Ξ2Ξ3 : t_ctx) (f1 : (Ξ βΆβ Β¬ A) β Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
s ββα΅£ f1 ββ f2 = s ββ f1 α΅£β f2) ->
forall (Ξ2Ξ3 : t_ctx) (f1 : Ξ β Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
Mu s ββα΅£ f1 `ββ f2 = Mu s `ββ f1 α΅£β f2
forall (Ξ : t_ctx) (A : pre_ty) (v : whn Ξ A),
(forall (Ξ2Ξ3 : t_ctx) (f1 : Ξ β Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
v `α΅₯βα΅£ f1 `α΅₯β f2 = v `α΅₯β f1 α΅£β f2) ->
forall (Ξ2Ξ3 : t_ctx) (f1 : Ξ β Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
Val v ββα΅£ f1 `ββ f2 = Val v `ββ f1 α΅£β f2
forall (Ξ : t_ctx) (A : pre_ty) (i : Ξ β Β¬ A)
(Ξ2Ξ3 : t_ctx) (f1 : Ξ β Ξ2) (f2 : Ξ2 =[ val ]> Ξ3),
VarR i ββα΅£ f1 `ββ f2 = VarR i `ββ f1 α΅£β f2
forall (Ξ : t_ctx) (A : pre_ty) (s : state (Ξ βΆβ β A)),
(forall (Ξ2Ξ3 : t_ctx) (f1 : (Ξ βΆβ β A) β Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
s ββα΅£ f1 ββ f2 = s ββ f1 α΅£β f2) ->
forall (Ξ2Ξ3 : t_ctx) (f1 : Ξ β Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
MuT s ββα΅£ f1 `ββ f2 = MuT s `ββ f1 α΅£β f2
forall (ΞΞ2Ξ3 : t_ctx) (f1 : Ξ β Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
Boom ββα΅£ f1 `ββ f2 = Boom `ββ f1 α΅£β f2
forall (Ξ : t_ctx) (AB : pre_ty) (v : whn Ξ A),
(forall (Ξ2Ξ3 : t_ctx) (f1 : Ξ β Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
v `α΅₯βα΅£ f1 `α΅₯β f2 = v `α΅₯β f1 α΅£β f2) ->
forallk : term Ξ Β¬ B,
(forall (Ξ2Ξ3 : t_ctx) (f1 : Ξ β Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
k ββα΅£ f1 `ββ f2 = k `ββ f1 α΅£β f2) ->
forall (Ξ2Ξ3 : t_ctx) (f1 : Ξ β Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
App v k ββα΅£ f1 `ββ f2 = App v k `ββ f1 α΅£β f2
forall (Ξ : t_ctx) (AB : pre_ty) (k : term Ξ Β¬ A),
(forall (Ξ2Ξ3 : t_ctx) (f1 : Ξ β Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
k ββα΅£ f1 `ββ f2 = k `ββ f1 α΅£β f2) ->
forall (Ξ2Ξ3 : t_ctx) (f1 : Ξ β Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
Fst k ββα΅£ f1 `ββ f2 = Fst k `ββ f1 α΅£β f2
forall (Ξ : t_ctx) (AB : pre_ty) (k : term Ξ Β¬ B),
(forall (Ξ2Ξ3 : t_ctx) (f1 : Ξ β Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
k ββα΅£ f1 `ββ f2 = k `ββ f1 α΅£β f2) ->
forall (Ξ2Ξ3 : t_ctx) (f1 : Ξ β Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
Snd k ββα΅£ f1 `ββ f2 = Snd k `ββ f1 α΅£β f2
forall (Ξ : t_ctx) (AB : pre_ty)
(s : state (Ξ βΆβ β A)),
(forall (Ξ2Ξ3 : t_ctx) (f1 : (Ξ βΆβ β A) β Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
s ββα΅£ f1 ββ f2 = s ββ f1 α΅£β f2) ->
forallt : state (Ξ βΆβ β B),
(forall (Ξ2Ξ3 : t_ctx) (f1 : (Ξ βΆβ β B) β Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
t ββα΅£ f1 ββ f2 = t ββ f1 α΅£β f2) ->
forall (Ξ2Ξ3 : t_ctx) (f1 : Ξ β Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
Case s t ββα΅£ f1 `ββ f2 = Case s t `ββ f1 α΅£β f2
forall (Ξ : t_ctx) (A : pre_ty) (i : Ξ β β A)
(Ξ2Ξ3 : t_ctx) (f1 : Ξ β Ξ2) (f2 : Ξ2 =[ val ]> Ξ3),
VarL i `α΅₯βα΅£ f1 `α΅₯β f2 = VarL i `α΅₯β f1 α΅£β f2
forall (Ξ : t_ctx) (AB : pre_ty) (v : whn Ξ A),
(forall (Ξ2Ξ3 : t_ctx) (f1 : Ξ β Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
v `α΅₯βα΅£ f1 `α΅₯β f2 = v `α΅₯β f1 α΅£β f2) ->
forall (Ξ2Ξ3 : t_ctx) (f1 : Ξ β Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
Inl v `α΅₯βα΅£ f1 `α΅₯β f2 = Inl v `α΅₯β f1 α΅£β f2
forall (Ξ : t_ctx) (AB : pre_ty) (v : whn Ξ B),
(forall (Ξ2Ξ3 : t_ctx) (f1 : Ξ β Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
v `α΅₯βα΅£ f1 `α΅₯β f2 = v `α΅₯β f1 α΅£β f2) ->
forall (Ξ2Ξ3 : t_ctx) (f1 : Ξ β Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
Inr v `α΅₯βα΅£ f1 `α΅₯β f2 = Inr v `α΅₯β f1 α΅£β f2
forall (ΞΞ2Ξ3 : t_ctx) (f1 : Ξ β Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
Tt `α΅₯βα΅£ f1 `α΅₯β f2 = Tt `α΅₯β f1 α΅£β f2
forall (Ξ : t_ctx) (AB : pre_ty)
(s : state (Ξ βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B)),
(forall (Ξ2Ξ3 : t_ctx)
(f1 : (Ξ βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B) β Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
s ββα΅£ f1 ββ f2 = s ββ f1 α΅£β f2) ->
forall (Ξ2Ξ3 : t_ctx) (f1 : Ξ β Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
Lam s `α΅₯βα΅£ f1 `α΅₯β f2 = Lam s `α΅₯β f1 α΅£β f2
forall (Ξ : t_ctx) (AB : pre_ty)
(s : state (Ξ βΆβ Β¬ A)),
(forall (Ξ2Ξ3 : t_ctx) (f1 : (Ξ βΆβ Β¬ A) β Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
s ββα΅£ f1 ββ f2 = s ββ f1 α΅£β f2) ->
forallt : state (Ξ βΆβ Β¬ B),
(forall (Ξ2Ξ3 : t_ctx) (f1 : (Ξ βΆβ Β¬ B) β Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
t ββα΅£ f1 ββ f2 = t ββ f1 α΅£β f2) ->
forall (Ξ2Ξ3 : t_ctx) (f1 : Ξ β Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
Pair s t `α΅₯βα΅£ f1 `α΅₯β f2 = Pair s t `α΅₯β f1 α΅£β f2
forall (Ξ : t_ctx) (A : pre_ty) (u : term Ξ β A),
(forall (Ξ2Ξ3 : t_ctx) (f1 : Ξ β Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
u ββα΅£ f1 `ββ f2 = u `ββ f1 α΅£β f2) ->
forallv : term Ξ Β¬ A,
(forall (Ξ2Ξ3 : t_ctx) (f1 : Ξ β Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
v ββα΅£ f1 `ββ f2 = v `ββ f1 α΅£β f2) ->
forall (Ξ2Ξ3 : t_ctx) (f1 : Ξ β Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
Cut u v ββα΅£ f1 ββ f2 = Cut u v ββ f1 α΅£β f2
Ξ: t_ctx A: pre_ty s: state (Ξ βΆβ Β¬ A) H: forall (Ξ2Ξ3 : t_ctx) (f1 : (Ξ βΆβ Β¬ A) β Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
s ββα΅£ f1 ββ f2 = s ββ f1 α΅£β f2 Ξ2, Ξ3: t_ctx f1: Ξ β Ξ2 f2: Ξ2 =[ val ]> Ξ3
s_subst (Ξ2 βΆβ Β¬ A) (s ββα΅£ r_shift1 f1) (Ξ3 βΆβ Β¬ A)
(a_shift1 f2) =
s_subst (Ξ βΆβ Β¬ A) s (Ξ3 βΆβ Β¬ A) (a_shift1 (f1 α΅£β f2))
Ξ: t_ctx A: pre_ty s: state (Ξ βΆβ β A) H: forall (Ξ2Ξ3 : t_ctx) (f1 : (Ξ βΆβ β A) β Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
s ββα΅£ f1 ββ f2 = s ββ f1 α΅£β f2 Ξ2, Ξ3: t_ctx f1: Ξ β Ξ2 f2: Ξ2 =[ val ]> Ξ3
s_subst (Ξ2 βΆβ β A) (s ββα΅£ r_shift1 f1) (Ξ3 βΆβ β A)
(a_shift1 f2) =
s_subst (Ξ βΆβ β A) s (Ξ3 βΆβ β A) (a_shift1 (f1 α΅£β f2))
Ξ: t_ctx A, B: pre_ty s: state (Ξ βΆβ β A) H: forall (Ξ2Ξ3 : t_ctx) (f1 : (Ξ βΆβ β A) β Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
s ββα΅£ f1 ββ f2 = s ββ f1 α΅£β f2 t: state (Ξ βΆβ β B) H0: forall (Ξ2Ξ3 : t_ctx) (f1 : (Ξ βΆβ β B) β Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
t ββα΅£ f1 ββ f2 = t ββ f1 α΅£β f2 Ξ2, Ξ3: t_ctx f1: Ξ β Ξ2 f2: Ξ2 =[ val ]> Ξ3
s_subst (Ξ2 βΆβ β A) (s ββα΅£ r_shift1 f1) (Ξ3 βΆβ β A)
(a_shift1 f2) =
s_subst (Ξ βΆβ β A) s (Ξ3 βΆβ β A) (a_shift1 (f1 α΅£β f2))
Ξ: t_ctx A, B: pre_ty s: state (Ξ βΆβ β A) H: forall (Ξ2Ξ3 : t_ctx) (f1 : (Ξ βΆβ β A) β Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
s ββα΅£ f1 ββ f2 = s ββ f1 α΅£β f2 t: state (Ξ βΆβ β B) H0: forall (Ξ2Ξ3 : t_ctx) (f1 : (Ξ βΆβ β B) β Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
t ββα΅£ f1 ββ f2 = t ββ f1 α΅£β f2 Ξ2, Ξ3: t_ctx f1: Ξ β Ξ2 f2: Ξ2 =[ val ]> Ξ3
s_subst (Ξ2 βΆβ β B) (t ββα΅£ r_shift1 f1) (Ξ3 βΆβ β B)
(a_shift1 f2) =
s_subst (Ξ βΆβ β B) t (Ξ3 βΆβ β B) (a_shift1 (f1 α΅£β f2))
Ξ: t_ctx A, B: pre_ty s: state (Ξ βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B) H: forall (Ξ2Ξ3 : t_ctx)
(f1 : (Ξ βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B) β Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
s ββα΅£ f1 ββ f2 = s ββ f1 α΅£β f2 Ξ2, Ξ3: t_ctx f1: Ξ β Ξ2 f2: Ξ2 =[ val ]> Ξ3
s_subst (Ξ2 βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B)
(s ββα΅£ r_shift3 f1) (Ξ3 βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B)
(a_shift3 f2) =
s_subst (Ξ βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B) s
(Ξ3 βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B)
(a_shift3 (f1 α΅£β f2))
Ξ: t_ctx A, B: pre_ty s: state (Ξ βΆβ Β¬ A) H: forall (Ξ2Ξ3 : t_ctx) (f1 : (Ξ βΆβ Β¬ A) β Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
s ββα΅£ f1 ββ f2 = s ββ f1 α΅£β f2 t: state (Ξ βΆβ Β¬ B) H0: forall (Ξ2Ξ3 : t_ctx) (f1 : (Ξ βΆβ Β¬ B) β Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
t ββα΅£ f1 ββ f2 = t ββ f1 α΅£β f2 Ξ2, Ξ3: t_ctx f1: Ξ β Ξ2 f2: Ξ2 =[ val ]> Ξ3
s_subst (Ξ2 βΆβ Β¬ A) (s ββα΅£ r_shift1 f1) (Ξ3 βΆβ Β¬ A)
(a_shift1 f2) =
s_subst (Ξ βΆβ Β¬ A) s (Ξ3 βΆβ Β¬ A) (a_shift1 (f1 α΅£β f2))
Ξ: t_ctx A, B: pre_ty s: state (Ξ βΆβ Β¬ A) H: forall (Ξ2Ξ3 : t_ctx) (f1 : (Ξ βΆβ Β¬ A) β Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
s ββα΅£ f1 ββ f2 = s ββ f1 α΅£β f2 t: state (Ξ βΆβ Β¬ B) H0: forall (Ξ2Ξ3 : t_ctx) (f1 : (Ξ βΆβ Β¬ B) β Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
t ββα΅£ f1 ββ f2 = t ββ f1 α΅£β f2 Ξ2, Ξ3: t_ctx f1: Ξ β Ξ2 f2: Ξ2 =[ val ]> Ξ3
s_subst (Ξ2 βΆβ Β¬ B) (t ββα΅£ r_shift1 f1) (Ξ3 βΆβ Β¬ B)
(a_shift1 f2) =
s_subst (Ξ βΆβ Β¬ B) t (Ξ3 βΆβ Β¬ B) (a_shift1 (f1 α΅£β f2))
all: first [ rewrite a_shift1_ren_l | rewrite a_shift3_ren_l ]; auto.Qed.
Ξ1, Ξ2: ctx ty Ξ3: t_ctx f1: Ξ1 β Ξ2 f2: Ξ2 =[ val ]> Ξ3 A: ty t: term Ξ1 A
t ββα΅£ f1 `ββ f2 = t `ββ f1 α΅£β f2
nowapply (term_ind_mut _ _ _ sub_ren_prf).Qed.
Ξ1, Ξ2: ctx ty Ξ3: t_ctx f1: Ξ1 β Ξ2 f2: Ξ2 =[ val ]> Ξ3 A: pre_ty v: whn Ξ1 A
v `α΅₯βα΅£ f1 `α΅₯β f2 = v `α΅₯β f1 α΅£β f2
nowapply (whn_ind_mut _ _ _ sub_ren_prf).Qed.
Ξ1, Ξ2: ctx ty Ξ3: t_ctx f1: Ξ1 β Ξ2 f2: Ξ2 =[ val ]> Ξ3 s: state Ξ1
s ββα΅£ f1 ββ f2 = s ββ f1 α΅£β f2
nowapply (state_ind_mut _ _ _ sub_ren_prf).Qed.
Ξ1, Ξ2: ctx ty Ξ3: t_ctx f1: Ξ1 β Ξ2 f2: Ξ2 =[ val ]> Ξ3 A: ty v: val Ξ1 A
v α΅₯βα΅£ f1 α΅₯β f2 = v α΅₯β f1 α΅£β f2
Ξ1, Ξ2: ctx ty Ξ3: t_ctx f1: Ξ1 β Ξ2 f2: Ξ2 =[ val ]> Ξ3 p: pre_ty v: val Ξ1 β p
v α΅₯βα΅£ f1 α΅₯β f2 = v α΅₯β f1 α΅£β f2
Ξ1, Ξ2: ctx ty Ξ3: t_ctx f1: Ξ1 β Ξ2 f2: Ξ2 =[ val ]> Ξ3 p: pre_ty v: val Ξ1 Β¬ p
v α΅₯βα΅£ f1 α΅₯β f2 = v α΅₯β f1 α΅£β f2
Ξ1, Ξ2: ctx ty Ξ3: t_ctx f1: Ξ1 β Ξ2 f2: Ξ2 =[ val ]> Ξ3 p: pre_ty v: val Ξ1 β p
v α΅₯βα΅£ f1 α΅₯β f2 = v α΅₯β f1 α΅£β f2
nowapply w_sub_ren.
Ξ1, Ξ2: ctx ty Ξ3: t_ctx f1: Ξ1 β Ξ2 f2: Ξ2 =[ val ]> Ξ3 p: pre_ty v: val Ξ1 Β¬ p
v α΅₯βα΅£ f1 α΅₯β f2 = v α΅₯β f1 α΅£β f2
nowapply t_sub_ren.Qed.
Ξ, Ξ: t_ctx f: Ξ =[ val ]> Ξ A: ty i: Ξ β A
Var i α΅₯β f = f A i
nowdestruct A.Qed.
Ξ1, Ξ2, Ξ3: t_ctx A: ty f1: Ξ1 =[ val ]> Ξ2 f2: Ξ2 =[ val ]> Ξ3
a_shift1 (f1 β f2) β‘β a_shift1 f1 β a_shift1 f2
Ξ: ctx ty Ξ2, Ξ3: t_ctx x: ty f1: Ξ =[ val ]> Ξ2 f2: Ξ2 =[ val ]> Ξ3
Var top =
v_subst (Ξ2 βΆβ x) x (Var top) (Ξ3 βΆβ x) (a_shift1 f2)
Ξ0: ctx ty Ξ2, Ξ3: t_ctx y: ty f1: Ξ0 =[ val ]> Ξ2 f2: Ξ2 =[ val ]> Ξ3 x: ty v: var x Ξ0
v_shift1 x (v_subst Ξ2 x (f1 x v) Ξ3 f2) =
v_subst (Ξ2 βΆβ y) x (v_shift1 x (f1 x v)) (Ξ3 βΆβ y)
(a_shift1 f2)
Ξ: ctx ty Ξ2, Ξ3: t_ctx x: ty f1: Ξ =[ val ]> Ξ2 f2: Ξ2 =[ val ]> Ξ3
Var top =
v_subst (Ξ2 βΆβ x) x (Var top) (Ξ3 βΆβ x) (a_shift1 f2)
nowrewrite v_sub_id_r.
Ξ0: ctx ty Ξ2, Ξ3: t_ctx y: ty f1: Ξ0 =[ val ]> Ξ2 f2: Ξ2 =[ val ]> Ξ3 x: ty v: var x Ξ0
v_shift1 x (v_subst Ξ2 x (f1 x v) Ξ3 f2) =
v_subst (Ξ2 βΆβ y) x (v_shift1 x (f1 x v)) (Ξ3 βΆβ y)
(a_shift1 f2)
Ξ1, Ξ2, Ξ3: t_ctx A, B, C: ty f1: Ξ1 =[ val ]> Ξ2 f2: Ξ2 =[ val ]> Ξ3
a_shift3 (f1 β f2) β‘β a_shift3 f1 β a_shift3 f2
Ξ0: ctx ty Ξ2, Ξ3: t_ctx y1, y0, y: ty f1: Ξ0 =[ val ]> Ξ2 f2: Ξ2 =[ val ]> Ξ3 a: ty v: var a Ξ0
v_shift3 a (v_subst Ξ2 a (f1 a v) Ξ3 f2) =
v_subst (Ξ2 βΆβ y1 βΆβ y0 βΆβ y) a (v_shift3 a (f1 a v))
(Ξ3 βΆβ y1 βΆβ y0 βΆβ y) (a_shift3 f2)
nowunfold v_shift3; rewrite v_ren_sub, v_sub_ren.Qed.Definitiont_sub_sub_PΞ1A (t : term Ξ1 A) : Prop :=
forallΞ2Ξ3 (f1 : Ξ1 =[val]> Ξ2) (f2 : Ξ2 =[val]> Ξ3),
(t `ββ f1) `ββ f2 = t `ββ (f1 β f2) .Definitionw_sub_sub_PΞ1A (v : whn Ξ1 A) : Prop :=
forallΞ2Ξ3 (f1 : Ξ1 =[val]> Ξ2) (f2 : Ξ2 =[val]> Ξ3),
(v `α΅₯β f1) `α΅₯β f2 = v `α΅₯β (f1 β f2) .Definitions_sub_sub_PΞ1 (s : state Ξ1) : Prop :=
forallΞ2Ξ3 (f1 : Ξ1 =[val]> Ξ2) (f2 : Ξ2 =[val]> Ξ3),
(s ββ f1) ββ f2 = s ββ (f1 β f2) .
syn_ind_args t_sub_sub_P w_sub_sub_P s_sub_sub_P
forall (Ξ : t_ctx) (A : pre_ty) (s : state (Ξ βΆβ Β¬ A)),
s_sub_sub_P (Ξ βΆβ Β¬ A) s -> t_sub_sub_P Ξ β A (Mu s)
forall (Ξ : t_ctx) (A : pre_ty) (v : whn Ξ A),
w_sub_sub_P Ξ A v -> t_sub_sub_P Ξ β A (Val v)
forall (Ξ : t_ctx) (A : pre_ty) (i : Ξ β Β¬ A),
t_sub_sub_P Ξ Β¬ A (VarR i)
forall (Ξ : t_ctx) (A : pre_ty) (s : state (Ξ βΆβ β A)),
s_sub_sub_P (Ξ βΆβ β A) s -> t_sub_sub_P Ξ Β¬ A (MuT s)
forallΞ : t_ctx, t_sub_sub_P Ξ Β¬ `0 Boom
forall (Ξ : t_ctx) (AB : pre_ty) (v : whn Ξ A),
w_sub_sub_P Ξ A v ->
forallk : term Ξ Β¬ B,
t_sub_sub_P Ξ Β¬ B k ->
t_sub_sub_P Ξ Β¬ (A `β B) (App v k)
forall (Ξ : t_ctx) (AB : pre_ty) (k : term Ξ Β¬ A),
t_sub_sub_P Ξ Β¬ A k ->
t_sub_sub_P Ξ Β¬ (A `Γ B) (Fst k)
forall (Ξ : t_ctx) (AB : pre_ty) (k : term Ξ Β¬ B),
t_sub_sub_P Ξ Β¬ B k ->
t_sub_sub_P Ξ Β¬ (A `Γ B) (Snd k)
forall (Ξ : t_ctx) (AB : pre_ty)
(s : state (Ξ βΆβ β A)),
s_sub_sub_P (Ξ βΆβ β A) s ->
forallt : state (Ξ βΆβ β B),
s_sub_sub_P (Ξ βΆβ β B) t ->
t_sub_sub_P Ξ Β¬ (A `+ B) (Case s t)
forall (Ξ : t_ctx) (A : pre_ty) (i : Ξ β β A),
w_sub_sub_P Ξ A (VarL i)
forall (Ξ : t_ctx) (AB : pre_ty) (v : whn Ξ A),
w_sub_sub_P Ξ A v -> w_sub_sub_P Ξ (A `+ B) (Inl v)
forall (Ξ : t_ctx) (AB : pre_ty) (v : whn Ξ B),
w_sub_sub_P Ξ B v -> w_sub_sub_P Ξ (A `+ B) (Inr v)
forallΞ : t_ctx, w_sub_sub_P Ξ `1 Tt
forall (Ξ : t_ctx) (AB : pre_ty)
(s : state (Ξ βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B)),
s_sub_sub_P (Ξ βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B) s ->
w_sub_sub_P Ξ (A `β B) (Lam s)
forall (Ξ : t_ctx) (AB : pre_ty)
(s : state (Ξ βΆβ Β¬ A)),
s_sub_sub_P (Ξ βΆβ Β¬ A) s ->
forallt : state (Ξ βΆβ Β¬ B),
s_sub_sub_P (Ξ βΆβ Β¬ B) t ->
w_sub_sub_P Ξ (A `Γ B) (Pair s t)
forall (Ξ : t_ctx) (A : pre_ty) (u : term Ξ β A),
t_sub_sub_P Ξ β A u ->
forallv : term Ξ Β¬ A,
t_sub_sub_P Ξ Β¬ A v -> s_sub_sub_P Ξ (Cut u v)
forall (Ξ : t_ctx) (A : pre_ty) (s : state (Ξ βΆβ Β¬ A)),
(forall (Ξ2Ξ3 : t_ctx) (f1 : (Ξ βΆβ Β¬ A) =[ val ]> Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
(s ββ f1) ββ f2 = s ββ f1 β f2) ->
forall (Ξ2Ξ3 : t_ctx) (f1 : Ξ =[ val ]> Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
(Mu s `ββ f1) `ββ f2 = Mu s `ββ f1 β f2
forall (Ξ : t_ctx) (A : pre_ty) (v : whn Ξ A),
(forall (Ξ2Ξ3 : t_ctx) (f1 : Ξ =[ val ]> Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
(v `α΅₯β f1) `α΅₯β f2 = v `α΅₯β f1 β f2) ->
forall (Ξ2Ξ3 : t_ctx) (f1 : Ξ =[ val ]> Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
(Val v `ββ f1) `ββ f2 = Val v `ββ f1 β f2
forall (Ξ : t_ctx) (A : pre_ty) (i : Ξ β Β¬ A)
(Ξ2Ξ3 : t_ctx) (f1 : Ξ =[ val ]> Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
(VarR i `ββ f1) `ββ f2 = VarR i `ββ f1 β f2
forall (Ξ : t_ctx) (A : pre_ty) (s : state (Ξ βΆβ β A)),
(forall (Ξ2Ξ3 : t_ctx) (f1 : (Ξ βΆβ β A) =[ val ]> Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
(s ββ f1) ββ f2 = s ββ f1 β f2) ->
forall (Ξ2Ξ3 : t_ctx) (f1 : Ξ =[ val ]> Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
(MuT s `ββ f1) `ββ f2 = MuT s `ββ f1 β f2
forall (ΞΞ2Ξ3 : t_ctx) (f1 : Ξ =[ val ]> Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
(Boom `ββ f1) `ββ f2 = Boom `ββ f1 β f2
forall (Ξ : t_ctx) (AB : pre_ty) (v : whn Ξ A),
(forall (Ξ2Ξ3 : t_ctx) (f1 : Ξ =[ val ]> Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
(v `α΅₯β f1) `α΅₯β f2 = v `α΅₯β f1 β f2) ->
forallk : term Ξ Β¬ B,
(forall (Ξ2Ξ3 : t_ctx) (f1 : Ξ =[ val ]> Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
(k `ββ f1) `ββ f2 = k `ββ f1 β f2) ->
forall (Ξ2Ξ3 : t_ctx) (f1 : Ξ =[ val ]> Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
(App v k `ββ f1) `ββ f2 = App v k `ββ f1 β f2
forall (Ξ : t_ctx) (AB : pre_ty) (k : term Ξ Β¬ A),
(forall (Ξ2Ξ3 : t_ctx) (f1 : Ξ =[ val ]> Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
(k `ββ f1) `ββ f2 = k `ββ f1 β f2) ->
forall (Ξ2Ξ3 : t_ctx) (f1 : Ξ =[ val ]> Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
(Fst k `ββ f1) `ββ f2 = Fst k `ββ f1 β f2
forall (Ξ : t_ctx) (AB : pre_ty) (k : term Ξ Β¬ B),
(forall (Ξ2Ξ3 : t_ctx) (f1 : Ξ =[ val ]> Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
(k `ββ f1) `ββ f2 = k `ββ f1 β f2) ->
forall (Ξ2Ξ3 : t_ctx) (f1 : Ξ =[ val ]> Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
(Snd k `ββ f1) `ββ f2 = Snd k `ββ f1 β f2
forall (Ξ : t_ctx) (AB : pre_ty)
(s : state (Ξ βΆβ β A)),
(forall (Ξ2Ξ3 : t_ctx) (f1 : (Ξ βΆβ β A) =[ val ]> Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
(s ββ f1) ββ f2 = s ββ f1 β f2) ->
forallt : state (Ξ βΆβ β B),
(forall (Ξ2Ξ3 : t_ctx) (f1 : (Ξ βΆβ β B) =[ val ]> Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
(t ββ f1) ββ f2 = t ββ f1 β f2) ->
forall (Ξ2Ξ3 : t_ctx) (f1 : Ξ =[ val ]> Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
(Case s t `ββ f1) `ββ f2 = Case s t `ββ f1 β f2
forall (Ξ : t_ctx) (A : pre_ty) (i : Ξ β β A)
(Ξ2Ξ3 : t_ctx) (f1 : Ξ =[ val ]> Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
(VarL i `α΅₯β f1) `α΅₯β f2 = VarL i `α΅₯β f1 β f2
forall (Ξ : t_ctx) (AB : pre_ty) (v : whn Ξ A),
(forall (Ξ2Ξ3 : t_ctx) (f1 : Ξ =[ val ]> Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
(v `α΅₯β f1) `α΅₯β f2 = v `α΅₯β f1 β f2) ->
forall (Ξ2Ξ3 : t_ctx) (f1 : Ξ =[ val ]> Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
(Inl v `α΅₯β f1) `α΅₯β f2 = Inl v `α΅₯β f1 β f2
forall (Ξ : t_ctx) (AB : pre_ty) (v : whn Ξ B),
(forall (Ξ2Ξ3 : t_ctx) (f1 : Ξ =[ val ]> Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
(v `α΅₯β f1) `α΅₯β f2 = v `α΅₯β f1 β f2) ->
forall (Ξ2Ξ3 : t_ctx) (f1 : Ξ =[ val ]> Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
(Inr v `α΅₯β f1) `α΅₯β f2 = Inr v `α΅₯β f1 β f2
forall (ΞΞ2Ξ3 : t_ctx) (f1 : Ξ =[ val ]> Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
(Tt `α΅₯β f1) `α΅₯β f2 = Tt `α΅₯β f1 β f2
forall (Ξ : t_ctx) (AB : pre_ty)
(s : state (Ξ βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B)),
(forall (Ξ2Ξ3 : t_ctx)
(f1 : (Ξ βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B) =[ val ]> Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
(s ββ f1) ββ f2 = s ββ f1 β f2) ->
forall (Ξ2Ξ3 : t_ctx) (f1 : Ξ =[ val ]> Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
(Lam s `α΅₯β f1) `α΅₯β f2 = Lam s `α΅₯β f1 β f2
forall (Ξ : t_ctx) (AB : pre_ty)
(s : state (Ξ βΆβ Β¬ A)),
(forall (Ξ2Ξ3 : t_ctx) (f1 : (Ξ βΆβ Β¬ A) =[ val ]> Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
(s ββ f1) ββ f2 = s ββ f1 β f2) ->
forallt : state (Ξ βΆβ Β¬ B),
(forall (Ξ2Ξ3 : t_ctx) (f1 : (Ξ βΆβ Β¬ B) =[ val ]> Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
(t ββ f1) ββ f2 = t ββ f1 β f2) ->
forall (Ξ2Ξ3 : t_ctx) (f1 : Ξ =[ val ]> Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
(Pair s t `α΅₯β f1) `α΅₯β f2 = Pair s t `α΅₯β f1 β f2
forall (Ξ : t_ctx) (A : pre_ty) (u : term Ξ β A),
(forall (Ξ2Ξ3 : t_ctx) (f1 : Ξ =[ val ]> Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
(u `ββ f1) `ββ f2 = u `ββ f1 β f2) ->
forallv : term Ξ Β¬ A,
(forall (Ξ2Ξ3 : t_ctx) (f1 : Ξ =[ val ]> Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
(v `ββ f1) `ββ f2 = v `ββ f1 β f2) ->
forall (Ξ2Ξ3 : t_ctx) (f1 : Ξ =[ val ]> Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
(Cut u v ββ f1) ββ f2 = Cut u v ββ f1 β f2
Ξ: t_ctx A: pre_ty s: state (Ξ βΆβ Β¬ A) H: forall (Ξ2Ξ3 : t_ctx)
(f1 : (Ξ βΆβ Β¬ A) =[ val ]> Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
(s ββ f1) ββ f2 = s ββ f1 β f2 Ξ2, Ξ3: t_ctx f1: Ξ =[ val ]> Ξ2 f2: Ξ2 =[ val ]> Ξ3
s_subst (Ξ2 βΆβ Β¬ A)
(s_subst (Ξ βΆβ Β¬ A) s (Ξ2 βΆβ Β¬ A) (a_shift1 f1))
(Ξ3 βΆβ Β¬ A) (a_shift1 f2) =
s_subst (Ξ βΆβ Β¬ A) s (Ξ3 βΆβ Β¬ A) (a_shift1 (f1 β f2))
Ξ: t_ctx A: pre_ty s: state (Ξ βΆβ β A) H: forall (Ξ2Ξ3 : t_ctx)
(f1 : (Ξ βΆβ β A) =[ val ]> Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
(s ββ f1) ββ f2 = s ββ f1 β f2 Ξ2, Ξ3: t_ctx f1: Ξ =[ val ]> Ξ2 f2: Ξ2 =[ val ]> Ξ3
s_subst (Ξ2 βΆβ β A)
(s_subst (Ξ βΆβ β A) s (Ξ2 βΆβ β A) (a_shift1 f1))
(Ξ3 βΆβ β A) (a_shift1 f2) =
s_subst (Ξ βΆβ β A) s (Ξ3 βΆβ β A) (a_shift1 (f1 β f2))
Ξ: t_ctx A, B: pre_ty s: state (Ξ βΆβ β A) H: forall (Ξ2Ξ3 : t_ctx)
(f1 : (Ξ βΆβ β A) =[ val ]> Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
(s ββ f1) ββ f2 = s ββ f1 β f2 t: state (Ξ βΆβ β B) H0: forall (Ξ2Ξ3 : t_ctx)
(f1 : (Ξ βΆβ β B) =[ val ]> Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
(t ββ f1) ββ f2 = t ββ f1 β f2 Ξ2, Ξ3: t_ctx f1: Ξ =[ val ]> Ξ2 f2: Ξ2 =[ val ]> Ξ3
s_subst (Ξ2 βΆβ β A)
(s_subst (Ξ βΆβ β A) s (Ξ2 βΆβ β A) (a_shift1 f1))
(Ξ3 βΆβ β A) (a_shift1 f2) =
s_subst (Ξ βΆβ β A) s (Ξ3 βΆβ β A) (a_shift1 (f1 β f2))
Ξ: t_ctx A, B: pre_ty s: state (Ξ βΆβ β A) H: forall (Ξ2Ξ3 : t_ctx)
(f1 : (Ξ βΆβ β A) =[ val ]> Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
(s ββ f1) ββ f2 = s ββ f1 β f2 t: state (Ξ βΆβ β B) H0: forall (Ξ2Ξ3 : t_ctx)
(f1 : (Ξ βΆβ β B) =[ val ]> Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
(t ββ f1) ββ f2 = t ββ f1 β f2 Ξ2, Ξ3: t_ctx f1: Ξ =[ val ]> Ξ2 f2: Ξ2 =[ val ]> Ξ3
s_subst (Ξ2 βΆβ β B)
(s_subst (Ξ βΆβ β B) t (Ξ2 βΆβ β B) (a_shift1 f1))
(Ξ3 βΆβ β B) (a_shift1 f2) =
s_subst (Ξ βΆβ β B) t (Ξ3 βΆβ β B) (a_shift1 (f1 β f2))
Ξ: t_ctx A, B: pre_ty s: state (Ξ βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B) H: forall (Ξ2Ξ3 : t_ctx)
(f1 : (Ξ βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B) =[ val
]> Ξ2) (f2 : Ξ2 =[ val ]> Ξ3),
(s ββ f1) ββ f2 = s ββ f1 β f2 Ξ2, Ξ3: t_ctx f1: Ξ =[ val ]> Ξ2 f2: Ξ2 =[ val ]> Ξ3
s_subst (Ξ2 βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B)
(s_subst (Ξ βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B) s
(Ξ2 βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B) (a_shift3 f1))
(Ξ3 βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B) (a_shift3 f2) =
s_subst (Ξ βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B) s
(Ξ3 βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B)
(a_shift3 (f1 β f2))
Ξ: t_ctx A, B: pre_ty s: state (Ξ βΆβ Β¬ A) H: forall (Ξ2Ξ3 : t_ctx)
(f1 : (Ξ βΆβ Β¬ A) =[ val ]> Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
(s ββ f1) ββ f2 = s ββ f1 β f2 t: state (Ξ βΆβ Β¬ B) H0: forall (Ξ2Ξ3 : t_ctx)
(f1 : (Ξ βΆβ Β¬ B) =[ val ]> Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
(t ββ f1) ββ f2 = t ββ f1 β f2 Ξ2, Ξ3: t_ctx f1: Ξ =[ val ]> Ξ2 f2: Ξ2 =[ val ]> Ξ3
s_subst (Ξ2 βΆβ Β¬ A)
(s_subst (Ξ βΆβ Β¬ A) s (Ξ2 βΆβ Β¬ A) (a_shift1 f1))
(Ξ3 βΆβ Β¬ A) (a_shift1 f2) =
s_subst (Ξ βΆβ Β¬ A) s (Ξ3 βΆβ Β¬ A) (a_shift1 (f1 β f2))
Ξ: t_ctx A, B: pre_ty s: state (Ξ βΆβ Β¬ A) H: forall (Ξ2Ξ3 : t_ctx)
(f1 : (Ξ βΆβ Β¬ A) =[ val ]> Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
(s ββ f1) ββ f2 = s ββ f1 β f2 t: state (Ξ βΆβ Β¬ B) H0: forall (Ξ2Ξ3 : t_ctx)
(f1 : (Ξ βΆβ Β¬ B) =[ val ]> Ξ2)
(f2 : Ξ2 =[ val ]> Ξ3),
(t ββ f1) ββ f2 = t ββ f1 β f2 Ξ2, Ξ3: t_ctx f1: Ξ =[ val ]> Ξ2 f2: Ξ2 =[ val ]> Ξ3
s_subst (Ξ2 βΆβ Β¬ B)
(s_subst (Ξ βΆβ Β¬ B) t (Ξ2 βΆβ Β¬ B) (a_shift1 f1))
(Ξ3 βΆβ Β¬ B) (a_shift1 f2) =
s_subst (Ξ βΆβ Β¬ B) t (Ξ3 βΆβ Β¬ B) (a_shift1 (f1 β f2))
all: first [ rewrite a_shift1_comp | rewrite a_shift3_comp ]; auto.Qed.
Ξ1, Ξ2, Ξ3: t_ctx f1: Ξ1 =[ val ]> Ξ2 f2: Ξ2 =[ val ]> Ξ3 A: ty t: term Ξ1 A
(t `ββ f1) `ββ f2 = t `ββ f1 β f2
nowapply (term_ind_mut _ _ _ sub_sub_prf).Qed.
Ξ1, Ξ2, Ξ3: t_ctx f1: Ξ1 =[ val ]> Ξ2 f2: Ξ2 =[ val ]> Ξ3 A: pre_ty v: whn Ξ1 A
(v `α΅₯β f1) `α΅₯β f2 = v `α΅₯β f1 β f2
nowapply (whn_ind_mut _ _ _ sub_sub_prf).Qed.
Ξ1, Ξ2, Ξ3: t_ctx f1: Ξ1 =[ val ]> Ξ2 f2: Ξ2 =[ val ]> Ξ3 s: state Ξ1
(s ββ f1) ββ f2 = s ββ f1 β f2
nowapply (state_ind_mut _ _ _ sub_sub_prf).Qed.
Ξ1, Ξ2, Ξ3: t_ctx f1: Ξ1 =[ val ]> Ξ2 f2: Ξ2 =[ val ]> Ξ3 A: ty v: val Ξ1 A
(v α΅₯β f1) α΅₯β f2 = v α΅₯β f1 β f2
Ξ1, Ξ2, Ξ3: t_ctx f1: Ξ1 =[ val ]> Ξ2 f2: Ξ2 =[ val ]> Ξ3 p: pre_ty v: val Ξ1 β p
(v α΅₯β f1) α΅₯β f2 = v α΅₯β f1 β f2
Ξ1, Ξ2, Ξ3: t_ctx f1: Ξ1 =[ val ]> Ξ2 f2: Ξ2 =[ val ]> Ξ3 p: pre_ty v: val Ξ1 Β¬ p
(v α΅₯β f1) α΅₯β f2 = v α΅₯β f1 β f2
Ξ1, Ξ2, Ξ3: t_ctx f1: Ξ1 =[ val ]> Ξ2 f2: Ξ2 =[ val ]> Ξ3 p: pre_ty v: val Ξ1 β p
(v α΅₯β f1) α΅₯β f2 = v α΅₯β f1 β f2
nowapply w_sub_sub.
Ξ1, Ξ2, Ξ3: t_ctx f1: Ξ1 =[ val ]> Ξ2 f2: Ξ2 =[ val ]> Ξ3 p: pre_ty v: val Ξ1 Β¬ p
(v α΅₯β f1) α΅₯β f2 = v α΅₯β f1 β f2
nowapply t_sub_sub.Qed.
Ξ1, Ξ2, Ξ3, Ξ4: t_ctx u: Ξ1 =[ val ]> Ξ2 v: Ξ2 =[ val ]> Ξ3 w: Ξ3 =[ val ]> Ξ4
(u β v) β w β‘β u β (v β w)
intros ? i; unfold a_comp; nowapply v_sub_sub.Qed.Definitiont_sub_id_l_PΞA (t : term Ξ A) : Prop := t `ββ Var = t.Definitionw_sub_id_l_PΞA (v : whn Ξ A) : Prop := v `α΅₯β Var = v.Definitions_sub_id_l_PΞ (s : state Ξ) : Prop := s ββ Var = s.
forall (Ξ : t_ctx) (A : pre_ty) (s : state (Ξ βΆβ Β¬ A)),
s_sub_id_l_P (Ξ βΆβ Β¬ A) s -> t_sub_id_l_P Ξ β A (Mu s)
forall (Ξ : t_ctx) (A : pre_ty) (v : whn Ξ A),
w_sub_id_l_P Ξ A v -> t_sub_id_l_P Ξ β A (Val v)
forall (Ξ : t_ctx) (A : pre_ty) (i : Ξ β Β¬ A),
t_sub_id_l_P Ξ Β¬ A (VarR i)
forall (Ξ : t_ctx) (A : pre_ty) (s : state (Ξ βΆβ β A)),
s_sub_id_l_P (Ξ βΆβ β A) s ->
t_sub_id_l_P Ξ Β¬ A (MuT s)
forallΞ : t_ctx, t_sub_id_l_P Ξ Β¬ `0 Boom
forall (Ξ : t_ctx) (AB : pre_ty) (v : whn Ξ A),
w_sub_id_l_P Ξ A v ->
forallk : term Ξ Β¬ B,
t_sub_id_l_P Ξ Β¬ B k ->
t_sub_id_l_P Ξ Β¬ (A `β B) (App v k)
forall (Ξ : t_ctx) (AB : pre_ty) (k : term Ξ Β¬ A),
t_sub_id_l_P Ξ Β¬ A k ->
t_sub_id_l_P Ξ Β¬ (A `Γ B) (Fst k)
forall (Ξ : t_ctx) (AB : pre_ty) (k : term Ξ Β¬ B),
t_sub_id_l_P Ξ Β¬ B k ->
t_sub_id_l_P Ξ Β¬ (A `Γ B) (Snd k)
forall (Ξ : t_ctx) (AB : pre_ty)
(s : state (Ξ βΆβ β A)),
s_sub_id_l_P (Ξ βΆβ β A) s ->
forallt : state (Ξ βΆβ β B),
s_sub_id_l_P (Ξ βΆβ β B) t ->
t_sub_id_l_P Ξ Β¬ (A `+ B) (Case s t)
forall (Ξ : t_ctx) (A : pre_ty) (i : Ξ β β A),
w_sub_id_l_P Ξ A (VarL i)
forall (Ξ : t_ctx) (AB : pre_ty) (v : whn Ξ A),
w_sub_id_l_P Ξ A v -> w_sub_id_l_P Ξ (A `+ B) (Inl v)
forall (Ξ : t_ctx) (AB : pre_ty) (v : whn Ξ B),
w_sub_id_l_P Ξ B v -> w_sub_id_l_P Ξ (A `+ B) (Inr v)
forallΞ : t_ctx, w_sub_id_l_P Ξ `1 Tt
forall (Ξ : t_ctx) (AB : pre_ty)
(s : state (Ξ βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B)),
s_sub_id_l_P (Ξ βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B) s ->
w_sub_id_l_P Ξ (A `β B) (Lam s)
forall (Ξ : t_ctx) (AB : pre_ty)
(s : state (Ξ βΆβ Β¬ A)),
s_sub_id_l_P (Ξ βΆβ Β¬ A) s ->
forallt : state (Ξ βΆβ Β¬ B),
s_sub_id_l_P (Ξ βΆβ Β¬ B) t ->
w_sub_id_l_P Ξ (A `Γ B) (Pair s t)
forall (Ξ : t_ctx) (A : pre_ty) (u : term Ξ β A),
t_sub_id_l_P Ξ β A u ->
forallv : term Ξ Β¬ A,
t_sub_id_l_P Ξ Β¬ A v -> s_sub_id_l_P Ξ (Cut u v)
forall (Ξ : t_ctx) (A : pre_ty) (s : state (Ξ βΆβ Β¬ A)),
s ββ Var = s -> Mu s `ββ Var = Mu s
forall (Ξ : t_ctx) (A : pre_ty) (v : whn Ξ A),
v `α΅₯β Var = v -> Val v `ββ Var = Val v
forall (Ξ : t_ctx) (A : pre_ty) (i : Ξ β Β¬ A),
VarR i `ββ Var = VarR i
forall (Ξ : t_ctx) (A : pre_ty) (s : state (Ξ βΆβ β A)),
s ββ Var = s -> MuT s `ββ Var = MuT s
forallΞ : t_ctx, Boom `ββ Var = Boom
forall (Ξ : t_ctx) (AB : pre_ty) (v : whn Ξ A),
v `α΅₯β Var = v ->
forallk : term Ξ Β¬ B,
k `ββ Var = k -> App v k `ββ Var = App v k
forall (Ξ : t_ctx) (AB : pre_ty) (k : term Ξ Β¬ A),
k `ββ Var = k -> Fst k `ββ Var = Fst k
forall (Ξ : t_ctx) (AB : pre_ty) (k : term Ξ Β¬ B),
k `ββ Var = k -> Snd k `ββ Var = Snd k
forall (Ξ : t_ctx) (AB : pre_ty)
(s : state (Ξ βΆβ β A)),
s ββ Var = s ->
forallt : state (Ξ βΆβ β B),
t ββ Var = t -> Case s t `ββ Var = Case s t
forall (Ξ : t_ctx) (A : pre_ty) (i : Ξ β β A),
VarL i `α΅₯β Var = VarL i
forall (Ξ : t_ctx) (AB : pre_ty) (v : whn Ξ A),
v `α΅₯β Var = v -> Inl v `α΅₯β Var = Inl v
forall (Ξ : t_ctx) (AB : pre_ty) (v : whn Ξ B),
v `α΅₯β Var = v -> Inr v `α΅₯β Var = Inr v
forallΞ : t_ctx, Tt `α΅₯β Var = Tt
forall (Ξ : t_ctx) (AB : pre_ty)
(s : state (Ξ βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B)),
s ββ Var = s -> Lam s `α΅₯β Var = Lam s
forall (Ξ : t_ctx) (AB : pre_ty)
(s : state (Ξ βΆβ Β¬ A)),
s ββ Var = s ->
forallt : state (Ξ βΆβ Β¬ B),
t ββ Var = t -> Pair s t `α΅₯β Var = Pair s t
forall (Ξ : t_ctx) (A : pre_ty) (u : term Ξ β A),
u `ββ Var = u ->
forallv : term Ξ Β¬ A,
v `ββ Var = v -> Cut u v ββ Var = Cut u v
Ξ: t_ctx A: pre_ty s: state (Ξ βΆβ Β¬ A) H: s ββ Var = s
s_subst (Ξ βΆβ Β¬ A) s (Ξ βΆβ Β¬ A) (a_shift1 Var) = s
Ξ: t_ctx A: pre_ty s: state (Ξ βΆβ β A) H: s ββ Var = s
s_subst (Ξ βΆβ β A) s (Ξ βΆβ β A) (a_shift1 Var) = s
Ξ: t_ctx A, B: pre_ty s: state (Ξ βΆβ β A) H: s ββ Var = s t: state (Ξ βΆβ β B) H0: t ββ Var = t
s_subst (Ξ βΆβ β A) s (Ξ βΆβ β A) (a_shift1 Var) = s
Ξ: t_ctx A, B: pre_ty s: state (Ξ βΆβ β A) H: s ββ Var = s t: state (Ξ βΆβ β B) H0: t ββ Var = t
s_subst (Ξ βΆβ β B) t (Ξ βΆβ β B) (a_shift1 Var) = t
Ξ: t_ctx A, B: pre_ty s: state (Ξ βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B) H: s ββ Var = s
s_subst (Ξ βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B) s
(Ξ βΆβ β (A `β B) βΆβ β A βΆβ Β¬ B) (a_shift3 Var) = s
Ξ: t_ctx A, B: pre_ty s: state (Ξ βΆβ Β¬ A) H: s ββ Var = s t: state (Ξ βΆβ Β¬ B) H0: t ββ Var = t
s_subst (Ξ βΆβ Β¬ A) s (Ξ βΆβ Β¬ A) (a_shift1 Var) = s
Ξ: t_ctx A, B: pre_ty s: state (Ξ βΆβ Β¬ A) H: s ββ Var = s t: state (Ξ βΆβ Β¬ B) H0: t ββ Var = t
s_subst (Ξ βΆβ Β¬ B) t (Ξ βΆβ Β¬ B) (a_shift1 Var) = t
all: first [ rewrite a_shift1_id | rewrite a_shift3_id ]; auto.Qed.
Ξ: t_ctx A: ty t: term Ξ A
t `ββ Var = t
nowapply (term_ind_mut _ _ _ sub_id_l_prf).Qed.
Ξ: t_ctx A: pre_ty v: whn Ξ A
v `α΅₯β Var = v
nowapply (whn_ind_mut _ _ _ sub_id_l_prf).Qed.
Ξ: t_ctx s: state Ξ
s ββ Var = s
nowapply (state_ind_mut _ _ _ sub_id_l_prf).Qed.
Ξ: t_ctx A: ty v: val Ξ A
v α΅₯β Var = v
Ξ: t_ctx p: pre_ty v: val Ξ β p
v α΅₯β Var = v
Ξ: t_ctx p: pre_ty v: val Ξ Β¬ p
v α΅₯β Var = v
Ξ: t_ctx p: pre_ty v: val Ξ β p
v α΅₯β Var = v
nowapply w_sub_id_l.
Ξ: t_ctx p: pre_ty v: val Ξ Β¬ p
v α΅₯β Var = v
nowapply t_sub_id_l.Qed.
Ξ, Ξ: t_ctx A: ty f: Ξ =[ val ]> Ξ v: val Ξ A
a_shift1 f β β[ v α΅₯β f] β‘β β[ v] β f
Ξ0: ctx ty Ξ: t_ctx a: ty f: Ξ0 =[ val ]> Ξ v: val Ξ0 a
v_subst (Ξ βΆβ a) a (Var top) Ξ β[ v_subst Ξ0 a v Ξ f] =
v_subst Ξ0 a v Ξ f
Ξ1: ctx ty Ξ: t_ctx y: ty f: Ξ1 =[ val ]> Ξ v: val Ξ1 y a: ty v0: var a Ξ1
v_subst (Ξ βΆβ y) a (v_shift1 a (f a v0)) Ξ
β[ v_subst Ξ1 y v Ξ f] = v_subst Ξ1 a (Var v0) Ξ f
Ξ0: ctx ty Ξ: t_ctx a: ty f: Ξ0 =[ val ]> Ξ v: val Ξ0 a
v_subst (Ξ βΆβ a) a (Var top) Ξ β[ v_subst Ξ0 a v Ξ f] =
v_subst Ξ0 a v Ξ f
nowrewrite v_sub_id_r.
Ξ1: ctx ty Ξ: t_ctx y: ty f: Ξ1 =[ val ]> Ξ v: val Ξ1 y a: ty v0: var a Ξ1
v_subst (Ξ βΆβ y) a (v_shift1 a (f a v0)) Ξ
β[ v_subst Ξ1 y v Ξ f] = v_subst Ξ1 a (Var v0) Ξ f
Ξ1: ctx ty Ξ: t_ctx y: ty f: Ξ1 =[ val ]> Ξ v: val Ξ1 y a: ty v0: var a Ξ1
f a v0 α΅₯β r_pop α΅£β β[ v_subst Ξ1 y v Ξ f] = f a v0
nowapply v_sub_id_l.Qed.
Ξ, Ξ: ctx ty A: ty f: Ξ β Ξ v: val Ξ A
r_shift1 f α΅£β β[ v α΅₯βα΅£ f] β‘β β[ v] βα΅£ f
Ξ1, Ξ: ctx ty y: ty f: Ξ1 β Ξ v: val Ξ1 y a: ty v0: var a Ξ1
(r_shift1 f α΅£β β[ v α΅₯βα΅£ f])%asgn a (pop v0) =
(β[ v] βα΅£ f)%asgn a (pop v0)
cbn; nowrewrite v_ren_id_r.Qed.
Ξ, Ξ: t_ctx A, B: ty f: Ξ =[ val ]> Ξ v: val Ξ A w: val (Ξ βΆβ A) B
(w α΅₯β a_shift1 f) α΅₯β β[ v α΅₯β f] = (w α΅₯β β[ v]) α΅₯β f
Ξ, Ξ: t_ctx A, B: ty f: Ξ =[ val ]> Ξ v: val Ξ A w: val (Ξ βΆβ A) B
w α΅₯β a_shift1 f β β[ v_subst Ξ A v Ξ f] =
w α΅₯β β[ v] β f
apply v_sub_eq; nowrewrite sub1_sub.Qed.
Ξ, Ξ: ctx ty A, B: ty f: Ξ β Ξ v: val Ξ A w: val (Ξ βΆβ A) B
w α΅₯βα΅£ r_shift1 f α΅₯β β[ v α΅₯βα΅£ f] = (w α΅₯β β[ v]) α΅₯βα΅£ f
Ξ, Ξ: ctx ty A, B: ty f: Ξ β Ξ v: val Ξ A w: val (Ξ βΆβ A) B
w α΅₯β r_shift1 f α΅£β β[ v α΅₯βα΅£ f] = w α΅₯β β[ v] βα΅£ f
apply v_sub_eq; nowrewrite sub1_ren.Qed.
Ξ, Ξ: t_ctx A: ty f: Ξ =[ val ]> Ξ v: val Ξ A s: state (Ξ βΆβ A)
(s ββ a_shift1 f) ββ β[ v α΅₯β f] = (s ββ β[ v]) ββ f
cbn; nowrewrite2 s_sub_sub, sub1_sub.Qed.
Ξ, Ξ: t_ctx A, B, C: ty f: Ξ =[ val ]> Ξ s: state (Ξ βΆβ A βΆβ B βΆβ C) u: val Ξ A v: val Ξ B w: val Ξ C
(s ββ a_shift3 f) ββ β[ u α΅₯β f, v α΅₯β f, w α΅₯β f] =
(s ββ β[ u, v, w]) ββ f
Ξ, Ξ: t_ctx A, B, C: ty f: Ξ =[ val ]> Ξ s: state (Ξ βΆβ A βΆβ B βΆβ C) u: val Ξ A v: val Ξ B w: val Ξ C
a_shift3 f
β β[ v_subst Ξ A u Ξ f, v_subst Ξ B v Ξ f,
v_subst Ξ C w Ξ f] β‘β β[ u, v, w] β f
Ξ, Ξ: t_ctx A, B, C: ty f: Ξ =[ val ]> Ξ s: state (Ξ βΆβ A βΆβ B βΆβ C) u: val Ξ A v: val Ξ B w: val Ξ C a: ty v0: Ξ βΆβ A βΆβ B βΆβ C β a
v_subst (Ξ βΆβ A βΆβ B βΆβ C) a (a_shift3 f a v0) Ξ
β[ v_subst Ξ A u Ξ f, v_subst Ξ B v Ξ f,
v_subst Ξ C w Ξ f] =
v_subst Ξ a (β[ u, v, w] a v0) Ξ f
Ξ1: ctx ty Ξ: t_ctx y1, y0, y: ty f: Ξ1 =[ val ]> Ξ s: state (Ξ1 βΆβ y1 βΆβ y0 βΆβ y) u: val Ξ1 y1 v: val Ξ1 y0 w: val Ξ1 y a: ty v0: var a Ξ1
v_subst (Ξ βΆβ y1 βΆβ y0 βΆβ y) a (v_shift3 a (f a v0)) Ξ
β[ v_subst Ξ1 y1 u Ξ f, v_subst Ξ1 y0 v Ξ f,
v_subst Ξ1 y w Ξ f] = v_subst Ξ1 a (Var v0) Ξ f
Ξ1: ctx ty Ξ: t_ctx y1, y0, y: ty f: Ξ1 =[ val ]> Ξ s: state (Ξ1 βΆβ y1 βΆβ y0 βΆβ y) u: val Ξ1 y1 v: val Ξ1 y0 w: val Ξ1 y a: ty v0: var a Ξ1
f a v0
α΅₯β ((r_pop α΅£β r_pop) α΅£β r_pop)
α΅£β β[ v_subst Ξ1 y1 u Ξ f, v_subst Ξ1 y0 v Ξ f,
v_subst Ξ1 y w Ξ f] = f a v0 α΅₯β Var
nowapply v_sub_eq.Qed.
Ξ, Ξ: ctx ty A: ty f: Ξ β Ξ v: val Ξ A s: state (Ξ βΆβ A)
s ββα΅£ r_shift1 f ββ β[ v α΅₯βα΅£ f] = (s ββ β[ v]) ββα΅£ f
p_of_w (a `+ b) (VarL i)
`α΅₯β p_dom_of_w (a `+ b) (VarL i) = VarL i
destruct (s_prf i).
Ξ: neg_ctx a, b: pre_ty v: whn Ξ a H: p_of_w a v `α΅₯β p_dom_of_w a v = v Heqcall: PInl (p_of_w a v) = p_of_w (a `+ b) (Inl v)
p_of_w (a `+ b) (Inl v)
`α΅₯β p_dom_of_w (a `+ b) (Inl v) = Inl v
nowcbn; f_equal.
Ξ: neg_ctx a, b: pre_ty v: whn Ξ b H: p_of_w b v `α΅₯β p_dom_of_w b v = v Heqcall: PInr (p_of_w b v) = p_of_w (a `+ b) (Inr v)
p_of_w (a `+ b) (Inr v)
`α΅₯β p_dom_of_w (a `+ b) (Inr v) = Inr v
nowcbn; f_equal.Qed.Equationsp_of_w_eq {Ξ : neg_ctx} A (p : pat βA) (e : pat_dom p =[val]> Ξ)
: p_of_w A ((p : val _ _) `α΅₯β e) = p :=
p_of_w_eq (a `+ b) (PInl v) e := f_equal PInl (p_of_w_eq _ v e) ;
p_of_w_eq (a `+ b) (PInr v) e := f_equal PInr (p_of_w_eq _ v e) ;
p_of_w_eq (`1) PTt e := eq_refl ;
p_of_w_eq (a `Γ b) PPair e := eq_refl ;
p_of_w_eq (a `β b) PLam e := eq_refl .
Ξ: neg_ctx A: pre_ty p: pat β A e: pat_dom p =[ val ]> Ξ
rew [funp : pat β A => pat_dom p =[ val ]> Ξ]
p_of_w_eq A p e in
p_dom_of_w A ((p : val (pat_dom p) β A) `α΅₯β e) β‘β e
Ξ: neg_ctx e: pat_dom PTt =[ val ]> Ξ Heqcall: eq_refl = p_of_w_eq `1 PTt e
! βΆβ e β `1 top β‘β e
Ξ: neg_ctx a, b: pre_ty e: pat_dom PPair =[ val ]> Ξ Heqcall: eq_refl = p_of_w_eq (a `Γ b) PPair e
! βΆβ e β (a `Γ b) top β‘β e
Ξ: neg_ctx a, b: pre_ty v: pat β a e: pat_dom (PInl v) =[ val ]> Ξ H: rew [funp : pat β a => pat_dom p =[ val ]> Ξ]
p_of_w_eq a v e in
p_dom_of_w a (v `α΅₯β e) β‘β e
rew [funp : pat β (a `+ b) => pat_dom p =[ val ]> Ξ]
f_equal PInl (p_of_w_eq a v e) in
p_dom_of_w a (v `α΅₯β e) β‘β e
Ξ: neg_ctx a, b: pre_ty v: pat β b e: pat_dom (PInr v) =[ val ]> Ξ H: rew [funp : pat β b => pat_dom p =[ val ]> Ξ]
p_of_w_eq b v e in
p_dom_of_w b (v `α΅₯β e) β‘β e
rew [funp : pat β (a `+ b) => pat_dom p =[ val ]> Ξ]
f_equal PInr (p_of_w_eq b v e) in
p_dom_of_w b (v `α΅₯β e) β‘β e
Ξ: neg_ctx a, b: pre_ty e: pat_dom PLam =[ val ]> Ξ Heqcall: eq_refl = p_of_w_eq (a `β b) PLam e
! βΆβ e β (a `β b) top β‘β e
Ξ: neg_ctx e: pat_dom PTt =[ val ]> Ξ Heqcall: eq_refl = p_of_w_eq `1 PTt e
Ξ: neg_ctx a, b: pre_ty v: pat β a e: pat_dom (PInl v) =[ val ]> Ξ H: rew [funp : pat β a => pat_dom p =[ val ]> Ξ]
p_of_w_eq a v e in p_dom_of_w a (v `α΅₯β e) β‘β e
rew [funp : pat β (a `+ b) => pat_dom p =[ val ]> Ξ]
f_equal PInl (p_of_w_eq a v e) in
p_dom_of_w a (v `α΅₯β e) β‘β e
Ξ: neg_ctx a, b: pre_ty v: pat β a e: pat_dom (PInl v) =[ val ]> Ξ H: rew [funp : pat β a => pat_dom p =[ val ]> Ξ]
p_of_w_eq a v e in p_dom_of_w a (v `α΅₯β e) β‘β e xx:= rew [funp : pat β (a `+ b) =>
pat_dom p =[ val ]> Ξ]
f_equal PInl (p_of_w_eq a v e) in
p_dom_of_w a (v `α΅₯β e): (funp : pat β (a `+ b) => pat_dom p =[ val ]> Ξ)
(PInl v)
xx β‘β e
Ξ: neg_ctx a, b: pre_ty v: pat β a e: pat_dom (PInl v) =[ val ]> Ξ H: rew [funp : pat β a => pat_dom p =[ val ]> Ξ]
p_of_w_eq a v e in p_dom_of_w a (v `α΅₯β e) β‘β e xx': (funp : pat β (a `+ b) => pat_dom p =[ val ]> Ξ) (PInl v) Heqxx': xx' =
rew [funp : pat β (a `+ b) =>
pat_dom p =[ val ]> Ξ]
f_equal PInl (p_of_w_eq a v e) in
p_dom_of_w a (v `α΅₯β e)
Ξ: neg_ctx a, b: pre_ty v: pat β b e: pat_dom (PInr v) =[ val ]> Ξ H: rew [funp : pat β b => pat_dom p =[ val ]> Ξ]
p_of_w_eq b v e in p_dom_of_w b (v `α΅₯β e) β‘β e
rew [funp : pat β (a `+ b) => pat_dom p =[ val ]> Ξ]
f_equal PInr (p_of_w_eq b v e) in
p_dom_of_w b (v `α΅₯β e) β‘β e
Ξ: neg_ctx a, b: pre_ty v: pat β b e: pat_dom (PInr v) =[ val ]> Ξ H: rew [funp : pat β b => pat_dom p =[ val ]> Ξ]
p_of_w_eq b v e in p_dom_of_w b (v `α΅₯β e) β‘β e xx:= rew [funp : pat β (a `+ b) =>
pat_dom p =[ val ]> Ξ]
f_equal PInr (p_of_w_eq b v e) in
p_dom_of_w b (v `α΅₯β e): (funp : pat β (a `+ b) => pat_dom p =[ val ]> Ξ)
(PInr v)
xx β‘β e
Ξ: neg_ctx a, b: pre_ty v: pat β b e: pat_dom (PInr v) =[ val ]> Ξ H: rew [funp : pat β b => pat_dom p =[ val ]> Ξ]
p_of_w_eq b v e in p_dom_of_w b (v `α΅₯β e) β‘β e xx': (funp : pat β (a `+ b) => pat_dom p =[ val ]> Ξ) (PInr v) Heqxx': xx' =
rew [funp : pat β (a `+ b) =>
pat_dom p =[ val ]> Ξ]
f_equal PInr (p_of_w_eq b v e) in
p_dom_of_w b (v `α΅₯β e)
Ξ2, Ξ1: neg_ctx A, B: pre_ty s: state (Ξ1 βΆβ β A) s0: state (Ξ1 βΆβ β B) r: Ξ1 β Ξ2 X: is_var (v_ren (Case s s0) r)
is_var (Case s s0)
Ξ2, Ξ1: neg_ctx A, B: pre_ty v: term Ξ1 Β¬ A IHv: forall (Ξ3 : neg_ctx) (p : pre_ty) (v0 : term Ξ3 Β¬ p),
Ξ1 ~= Ξ3 ->
Β¬ A = Β¬ p -> v ~= v0 -> forallr : Ξ3 β Ξ2, is_var (v_ren v0 r) -> is_var v0 r: Ξ1 β Ξ2 X: is_var (v_ren (Fst v) r)
is_var (Fst v)
Ξ2, Ξ1: neg_ctx A, B: pre_ty v: term Ξ1 Β¬ B IHv: forall (Ξ3 : neg_ctx) (p : pre_ty) (v0 : term Ξ3 Β¬ p),
Ξ1 ~= Ξ3 ->
Β¬ B = Β¬ p -> v ~= v0 -> forallr : Ξ3 β Ξ2, is_var (v_ren v0 r) -> is_var v0 r: Ξ1 β Ξ2 X: is_var (v_ren (Snd v) r)
is_var (Snd v)
Ξ2, Ξ1: neg_ctx A, B: pre_ty w: whn Ξ1 A v: term Ξ1 Β¬ B IHv: forall (Ξ3 : neg_ctx) (p : pre_ty) (v0 : term Ξ3 Β¬ p),
Ξ1 ~= Ξ3 ->
Β¬ B = Β¬ p -> v ~= v0 -> forallr : Ξ3 β Ξ2, is_var (v_ren v0 r) -> is_var v0 r: Ξ1 β Ξ2 X: is_var (v_ren (App w v) r)
is_var (App w v)
all: trynowdependent destruction X; exact (Vvar _).all: dependent induction w; dependent destruction X; exact (Vvar _).Qed.#[global] Instancesysl_machine : machine val_n state_n op_copat :=
{| Machine.eval := @eval ; oapp := @p_app |} .From Coinduction Require Import coinduction lattice rel tactics.Ltacrefold_eval :=
change (Structure.iter _ _ ?a) with (eval a);
change (Structure.subst (funpat : T1 => let'T1_0 := pat in?f) T1_0 ?u)
with (bind_delay' u f).Definitionupg_v {Ξ} {A : pre_ty} : whn Ξ A -> val Ξ βA := funv => v.Definitionupg_k {Ξ} {A : pre_ty} : term Ξ Β¬A -> val Ξ Β¬A := funv => v.Definitiondwn_v {Ξ} {A : pre_ty} : val Ξ βA -> whn Ξ A := funv => v.Definitiondwn_k {Ξ} {A : pre_ty} : val Ξ Β¬A -> term Ξ Β¬A := funv => v.
Ξ: neg_ctx A: pre_ty i: Ξ β Β¬ A p: pat β A Ξ³: pat_dom p =[ val ]> Ξ
nf_eq
(i
β w_split A
(dwn_v ((p : val (pat_dom p) β A) `α΅₯β Ξ³)))
(i β (p : op_copat Β¬ A) β¦ Ξ³ β¦)
Ξ: neg_ctx A: pre_ty i: Ξ β Β¬ A p: pat β A Ξ³: pat_dom p =[ val ]> Ξ
nf_eq
(i β p_of_w A (p `α΅₯β Ξ³) β¦ p_dom_of_w A (p `α΅₯β Ξ³) β¦)
(i β p β¦ Ξ³ β¦)
Ξ: neg_ctx A: pre_ty i: Ξ β Β¬ A p: pat β A Ξ³: pat_dom p =[ val ]> Ξ H: rew [funp : pat β A => pat_dom p =[ val ]> Ξ]
p_of_w_eq A p Ξ³ in
p_dom_of_w A ((p : val (pat_dom p) β A) `α΅₯β Ξ³)
β‘β Ξ³
nf_eq
(i β p_of_w A (p `α΅₯β Ξ³) β¦ p_dom_of_w A (p `α΅₯β Ξ³) β¦)
(i β p β¦ Ξ³ β¦)
Ξ: neg_ctx A: pre_ty i: Ξ β Β¬ A p: pat β A Ξ³: pat_dom p =[ val ]> Ξ H':= p_of_w_eq A p Ξ³: p_of_w A ((p : val (pat_dom p) β A) `α΅₯β Ξ³) = p H: rew [funp : pat β A => pat_dom p =[ val ]> Ξ]
H' in
p_dom_of_w A ((p : val (pat_dom p) β A) `α΅₯β Ξ³)
β‘β Ξ³
nf_eq
(i β p_of_w A (p `α΅₯β Ξ³) β¦ p_dom_of_w A (p `α΅₯β Ξ³) β¦)
(i β p β¦ Ξ³ β¦)
Ξ: neg_ctx A: pre_ty i: Ξ β Β¬ A p: pat β A Ξ³: pat_dom p =[ val ]> Ξ H':= p_of_w_eq A p Ξ³: p_of_w A ((p : val (pat_dom p) β A) `α΅₯β Ξ³) = p a:= p_dom_of_w A (p `α΅₯β Ξ³): pat_dom (p_of_w A (p `α΅₯β Ξ³)) =[ val ]> Ξ H: rew [funp : pat β A => pat_dom p =[ val ]> Ξ]
H' in a β‘β Ξ³
nf_eq (i β p_of_w A (p `α΅₯β Ξ³) β¦ a β¦) (i β p β¦ Ξ³ β¦)
Ξ: neg_ctx A: pre_ty i: Ξ β Β¬ A p: pat β A Ξ³: pat_dom p =[ val ]> Ξ H':= p_of_w_eq A p Ξ³: p_of_w A ((p : val (pat_dom p) β A) `α΅₯β Ξ³) = p a': pat_dom (p_of_w A (p `α΅₯β Ξ³)) =[ val ]> Ξ H: rew [funp : pat β A => pat_dom p =[ val ]> Ξ]
H' in a' β‘β Ξ³
nf_eq (i β p_of_w A (p `α΅₯β Ξ³) β¦ a' β¦) (i β p β¦ Ξ³ β¦)
revert a' H; rewrite H'; intros; noweconstructor.Qed.
machine_laws val_n state_n op_copat
forall (Ξ : neg_ctx) (x : ty) (v : val Ξ x)
(o : op_copat x),
Proper (asgn_eq (dom o) Ξ ==> eq) (oapp v o)
forall (Ξ1Ξ2 : neg_ctx) (x : ty) (v : val Ξ1 x)
(o : op_copat x) (a : dom o =[ val_n ]> Ξ1)
(b : Ξ1 =[ val_n ]> Ξ2),
v β o β¦ a β¦ ββ b = (v α΅₯β b) β o β¦ a β b β¦
forall (ΞΞ : neg_ctx) (c : state Ξ)
(a : Ξ =[ val_n ]> Ξ),
Machine.eval (c ββ a)
β bind_delay' (Machine.eval c)
(funn : nf op_copat val_n Ξ =>
Machine.eval (emb n ββ a))
forall (Ξ : neg_ctx) (u : nf op_copat val_n Ξ),
Machine.eval (emb u) β ret_delay u
well_founded head_inst_nostep
forall (Ξ : neg_ctx) (x : ty) (v : val Ξ x)
(o : op_copat x),
Proper (asgn_eq (dom o) Ξ ==> eq) (oapp v o)
intros; apply p_app_eq.
forall (Ξ1Ξ2 : neg_ctx) (x : ty) (v : val Ξ1 x)
(o : op_copat x) (a : dom o =[ val_n ]> Ξ1)
(b : Ξ1 =[ val_n ]> Ξ2),
v β o β¦ a β¦ ββ b = (v α΅₯β b) β o β¦ a β b β¦
Ξ1, Ξ2: neg_ctx p: pre_ty v: val Ξ1 β p o: op_copat β p a: dom o =[ val_n ]> Ξ1 b: Ξ1 =[ val_n ]> Ξ2
Cut (Val (v `α΅₯β b)) ((o `ββ a) `ββ b) =
Cut (Val (v `α΅₯β b)) (o `ββ a β b)
Ξ1, Ξ2: neg_ctx p: pre_ty v: val Ξ1 Β¬ p o: op_copat Β¬ p a: dom o =[ val_n ]> Ξ1 b: Ξ1 =[ val_n ]> Ξ2
Cut (Val ((o `α΅₯β a) `α΅₯β b)) (v `ββ b) =
Cut (Val (o `α΅₯β a β b)) (v `ββ b)
Ξ1, Ξ2: neg_ctx p: pre_ty v: val Ξ1 Β¬ p o: op_copat Β¬ p a: dom o =[ val_n ]> Ξ1 b: Ξ1 =[ val_n ]> Ξ2
Cut (Val ((o `α΅₯β a) `α΅₯β b)) (v `ββ b) =
Cut (Val (o `α΅₯β a β b)) (v `ββ b)
nowrewrite (w_sub_sub _ _ _ _).
forall (ΞΞ : neg_ctx) (c : state Ξ)
(a : Ξ =[ val_n ]> Ξ),
Machine.eval (c ββ a)
β bind_delay' (Machine.eval c)
(funn : nf op_copat val_n Ξ =>
Machine.eval (emb n ββ a))
forall (Ξ : neg_ctx) (u : nf op_copat val_n Ξ),
Machine.eval (emb u) β ret_delay u
Ξ: neg_ctx A: ty i: Ξ β A o: op_copat A Ξ³: dom o =[ val_n ]> Ξ
eval (Cut' (Var i) (o `ββ Ξ³))
β ret_delay (i β o β¦ Ξ³ β¦)
Ξ: neg_ctx A: ty i: Ξ β A o: pat A β Ξ³: dom o =[ val_n ]> Ξ eqargs: {| pr1 := β `1; pr2 := PTt |} =
{| pr1 := A β ; pr2 := o |} H0: β `1 = A β H1: β `1,' PTt = A β ,' o
eval
(Cut' (Var i)
(rew [funprojs : sigma (funA : ty => pat A) =>
val (pat_dom (pr2 projs)) (pr1 projs)]
eqargs in VarL Ctx.top `ββ Ξ³))
β ret_delay (i β o β¦ Ξ³ β¦)
a, b: pre_ty Ξ: neg_ctx A: ty i: Ξ β A o: pat A β Ξ³: dom o =[ val_n ]> Ξ eqargs: {| pr1 := β (a `Γ b); pr2 := PPair |} =
{| pr1 := A β ; pr2 := o |} H0: β (a `Γ b) = A β H1: β (a `Γ b),' PPair = A β ,' o
eval
(Cut' (Var i)
(rew [funprojs : sigma (funA : ty => pat A) =>
val (pat_dom (pr2 projs)) (pr1 projs)]
eqargs in VarL Ctx.top `ββ Ξ³))
β ret_delay (i β o β¦ Ξ³ β¦)
a0, b0: pre_ty u: pat β a0 H: forall (Ξ : neg_ctx) (A : ty)
(i : Ξ β A) (o : pat A β )
(Ξ³ : dom o =[ val_n ]> Ξ)
(eqargs : {| pr1 := β a0; pr2 := u |} =
{| pr1 := A β ; pr2 := o |}),
rew [funprojs : sigma (funA0 : ty => pat A0) =>
val (pat_dom (pr2 projs)) (pr1 projs)]
eqargs in u = o ->
eval (Cut' (Var i) (o `ββ Ξ³))
β ret_delay (i β o β¦ Ξ³ β¦) Ξ: neg_ctx A: ty i: Ξ β A o: pat A β Ξ³: dom o =[ val_n ]> Ξ eqargs: {| pr1 := β (a0 `+ b0); pr2 := PInl u |} =
{| pr1 := A β ; pr2 := o |} H1: β (a0 `+ b0) = A β H2: β (a0 `+ b0),' PInl u = A β ,' o
eval
(Cut' (Var i)
(rew [funprojs : sigma (funA : ty => pat A) =>
val (pat_dom (pr2 projs)) (pr1 projs)]
eqargs in Inl u `ββ Ξ³))
β ret_delay (i β o β¦ Ξ³ β¦)
a1, b1: pre_ty u: pat β b1 H: forall (Ξ : neg_ctx) (A : ty)
(i : Ξ β A) (o : pat A β )
(Ξ³ : dom o =[ val_n ]> Ξ)
(eqargs : {| pr1 := β b1; pr2 := u |} =
{| pr1 := A β ; pr2 := o |}),
rew [funprojs : sigma (funA0 : ty => pat A0) =>
val (pat_dom (pr2 projs)) (pr1 projs)]
eqargs in u = o ->
eval (Cut' (Var i) (o `ββ Ξ³))
β ret_delay (i β o β¦ Ξ³ β¦) Ξ: neg_ctx A: ty i: Ξ β A o: pat A β Ξ³: dom o =[ val_n ]> Ξ eqargs: {| pr1 := β (a1 `+ b1); pr2 := PInr u |} =
{| pr1 := A β ; pr2 := o |} H1: β (a1 `+ b1) = A β H2: β (a1 `+ b1),' PInr u = A β ,' o
eval
(Cut' (Var i)
(rew [funprojs : sigma (funA : ty => pat A) =>
val (pat_dom (pr2 projs)) (pr1 projs)]
eqargs in Inr u `ββ Ξ³))
β ret_delay (i β o β¦ Ξ³ β¦)
a2, b2: pre_ty Ξ: neg_ctx A: ty i: Ξ β A o: pat A β Ξ³: dom o =[ val_n ]> Ξ eqargs: {| pr1 := β (a2 `β b2); pr2 := PLam |} =
{| pr1 := A β ; pr2 := o |} H0: β (a2 `β b2) = A β H1: β (a2 `β b2),' PLam = A β ,' o
eval
(Cut' (Var i)
(rew [funprojs : sigma (funA : ty => pat A) =>
val (pat_dom (pr2 projs)) (pr1 projs)]
eqargs in VarL Ctx.top `ββ Ξ³))
β ret_delay (i β o β¦ Ξ³ β¦)
a3, b3: pre_ty Ξ: neg_ctx A: ty i: Ξ β A o: pat A β Ξ³: dom o =[ val_n ]> Ξ eqargs: {| pr1 := Β¬ (a3 `Γ b3); pr2 := PFst |} =
{| pr1 := A β ; pr2 := o |} H0: Β¬ (a3 `Γ b3) = A β H1: Β¬ (a3 `Γ b3),' PFst = A β ,' o
eval
(Cut' (Var i)
(rew [funprojs : sigma (funA : ty => pat A) =>
val (pat_dom (pr2 projs)) (pr1 projs)]
eqargs in Fst (VarR Ctx.top) `ββ Ξ³))
β ret_delay (i β o β¦ Ξ³ β¦)
a4, b4: pre_ty Ξ: neg_ctx A: ty i: Ξ β A o: pat A β Ξ³: dom o =[ val_n ]> Ξ eqargs: {| pr1 := Β¬ (a4 `Γ b4); pr2 := PSnd |} =
{| pr1 := A β ; pr2 := o |} H0: Β¬ (a4 `Γ b4) = A β H1: Β¬ (a4 `Γ b4),' PSnd = A β ,' o
eval
(Cut' (Var i)
(rew [funprojs : sigma (funA : ty => pat A) =>
val (pat_dom (pr2 projs)) (pr1 projs)]
eqargs in Snd (VarR Ctx.top) `ββ Ξ³))
β ret_delay (i β o β¦ Ξ³ β¦)
a5, b5: pre_ty v: pat β a5 H: forall (Ξ : neg_ctx) (A : ty)
(i : Ξ β A) (o : pat A β )
(Ξ³ : dom o =[ val_n ]> Ξ)
(eqargs : {| pr1 := β a5; pr2 := v |} =
{| pr1 := A β ; pr2 := o |}),
rew [funprojs : sigma (funA0 : ty => pat A0) =>
val (pat_dom (pr2 projs)) (pr1 projs)]
eqargs in v = o ->
eval (Cut' (Var i) (o `ββ Ξ³))
β ret_delay (i β o β¦ Ξ³ β¦) Ξ: neg_ctx A: ty i: Ξ β A o: pat A β Ξ³: dom o =[ val_n ]> Ξ eqargs: {| pr1 := Β¬ (a5 `β b5); pr2 := PApp v |} =
{| pr1 := A β ; pr2 := o |} H1: Β¬ (a5 `β b5) = A β H2: Β¬ (a5 `β b5),' PApp v = A β ,' o
eval
(Cut' (Var i)
(rew [funprojs : sigma (funA : ty => pat A) =>
val (pat_dom (pr2 projs)) (pr1 projs)]
eqargs in App (v `α΅₯βα΅£ r_pop) (VarR Ctx.top)
`ββ Ξ³)) β ret_delay (i β o β¦ Ξ³ β¦)
Ξ: neg_ctx i: Ξ β Β¬ `1 o: pat (Β¬ `1) β Ξ³: dom o =[ val_n ]> Ξ eqargs: {| pr1 := β `1; pr2 := PTt |} =
{| pr1 := (Β¬ `1) β ; pr2 := o |} H1: β `1,' PTt = (Β¬ `1) β ,' o
eval
(Cut' (Var i)
(rew [funprojs : sigma (funA : ty => pat A) =>
val (pat_dom (pr2 projs)) (pr1 projs)]
eqargs in VarL Ctx.top `ββ Ξ³))
β ret_delay (i β o β¦ Ξ³ β¦)
a, b: pre_ty Ξ: neg_ctx i: Ξ β Β¬ (a `Γ b) o: pat (Β¬ (a `Γ b)) β Ξ³: dom o =[ val_n ]> Ξ eqargs: {| pr1 := β (a `Γ b); pr2 := PPair |} =
{| pr1 := (Β¬ (a `Γ b)) β ; pr2 := o |} H1: β (a `Γ b),' PPair = (Β¬ (a `Γ b)) β ,' o
eval
(Cut' (Var i)
(rew [funprojs : sigma (funA : ty => pat A) =>
val (pat_dom (pr2 projs)) (pr1 projs)]
eqargs in VarL Ctx.top `ββ Ξ³))
β ret_delay (i β o β¦ Ξ³ β¦)
a0, b0: pre_ty u: pat β a0 H: forall (Ξ : neg_ctx) (A : ty)
(i : Ξ β A) (o : pat A β )
(Ξ³ : dom o =[ val_n ]> Ξ)
(eqargs : {| pr1 := β a0; pr2 := u |} =
{| pr1 := A β ; pr2 := o |}),
rew [funprojs : sigma (funA0 : ty => pat A0) =>
val (pat_dom (pr2 projs)) (pr1 projs)]
eqargs in u = o ->
eval (Cut' (Var i) (o `ββ Ξ³))
β ret_delay (i β o β¦ Ξ³ β¦) Ξ: neg_ctx i: Ξ β Β¬ (a0 `+ b0) o: pat (Β¬ (a0 `+ b0)) β Ξ³: dom o =[ val_n ]> Ξ eqargs: {| pr1 := β (a0 `+ b0); pr2 := PInl u |} =
{| pr1 := (Β¬ (a0 `+ b0)) β ; pr2 := o |} H2: β (a0 `+ b0),' PInl u = (Β¬ (a0 `+ b0)) β ,' o
eval
(Cut' (Var i)
(rew [funprojs : sigma (funA : ty => pat A) =>
val (pat_dom (pr2 projs)) (pr1 projs)]
eqargs in Inl u `ββ Ξ³))
β ret_delay (i β o β¦ Ξ³ β¦)
a1, b1: pre_ty u: pat β b1 H: forall (Ξ : neg_ctx) (A : ty)
(i : Ξ β A) (o : pat A β )
(Ξ³ : dom o =[ val_n ]> Ξ)
(eqargs : {| pr1 := β b1; pr2 := u |} =
{| pr1 := A β ; pr2 := o |}),
rew [funprojs : sigma (funA0 : ty => pat A0) =>
val (pat_dom (pr2 projs)) (pr1 projs)]
eqargs in u = o ->
eval (Cut' (Var i) (o `ββ Ξ³))
β ret_delay (i β o β¦ Ξ³ β¦) Ξ: neg_ctx i: Ξ β Β¬ (a1 `+ b1) o: pat (Β¬ (a1 `+ b1)) β Ξ³: dom o =[ val_n ]> Ξ eqargs: {| pr1 := β (a1 `+ b1); pr2 := PInr u |} =
{| pr1 := (Β¬ (a1 `+ b1)) β ; pr2 := o |} H2: β (a1 `+ b1),' PInr u = (Β¬ (a1 `+ b1)) β ,' o
eval
(Cut' (Var i)
(rew [funprojs : sigma (funA : ty => pat A) =>
val (pat_dom (pr2 projs)) (pr1 projs)]
eqargs in Inr u `ββ Ξ³))
β ret_delay (i β o β¦ Ξ³ β¦)
eval
(Cut' (Var i)
(rew [funprojs : sigma (funA : ty => pat A) =>
val (pat_dom (pr2 projs)) (pr1 projs)]
eqargs in VarL Ctx.top `ββ Ξ³))
β ret_delay (i β o β¦ Ξ³ β¦)
eval
(Cut' (Var i)
(rew [funprojs : sigma (funA : ty => pat A) =>
val (pat_dom (pr2 projs)) (pr1 projs)]
eqargs in Snd (VarR Ctx.top) `ββ Ξ³))
β ret_delay (i β o β¦ Ξ³ β¦)
a5, b5: pre_ty v: pat β a5 H: forall (Ξ : neg_ctx) (A : ty)
(i : Ξ β A) (o : pat A β )
(Ξ³ : dom o =[ val_n ]> Ξ)
(eqargs : {| pr1 := β a5; pr2 := v |} =
{| pr1 := A β ; pr2 := o |}),
rew [funprojs : sigma (funA0 : ty => pat A0) =>
val (pat_dom (pr2 projs)) (pr1 projs)]
eqargs in v = o ->
eval (Cut' (Var i) (o `ββ Ξ³))
β ret_delay (i β o β¦ Ξ³ β¦) Ξ: neg_ctx i: Ξ β β (a5 `β b5) o: pat (β (a5 `β b5)) β Ξ³: dom o =[ val_n ]> Ξ eqargs: {| pr1 := Β¬ (a5 `β b5); pr2 := PApp v |} =
{| pr1 := (β (a5 `β b5)) β ; pr2 := o |} H2: Β¬ (a5 `β b5),' PApp v = (β (a5 `β b5)) β ,' o
eval
(Cut' (Var i)
(rew [funprojs : sigma (funA : ty => pat A) =>
val (pat_dom (pr2 projs)) (pr1 projs)]
eqargs in App (v `α΅₯βα΅£ r_pop) (VarR Ctx.top)
`ββ Ξ³)) β ret_delay (i β o β¦ Ξ³ β¦)
Ξ: neg_ctx i: Ξ β Β¬ `1 Ξ³: dom PTt =[ val_n ]> Ξ H1: β `1,' PTt = (Β¬ `1) β ,' PTt
eval (Cut (Val (Ξ³ β `1 Ctx.top)) (Var i))
β ret_delay (i β PTt β¦ Ξ³ β¦)
a, b: pre_ty Ξ: neg_ctx i: Ξ β Β¬ (a `Γ b) Ξ³: dom PPair =[ val_n ]> Ξ H1: β (a `Γ b),' PPair = (Β¬ (a `Γ b)) β ,' PPair
eval (Cut (Val (Ξ³ β (a `Γ b) Ctx.top)) (Var i))
β ret_delay (i β PPair β¦ Ξ³ β¦)
a0, b0: pre_ty u: pat β a0 H: forall (Ξ : neg_ctx) (A : ty) (i : Ξ β A)
(o : pat A β ) (Ξ³ : dom o =[ val_n ]> Ξ)
(eqargs : {| pr1 := β a0; pr2 := u |} =
{| pr1 := A β ; pr2 := o |}),
rew [funprojs : sigma (funA0 : ty => pat A0) =>
val (pat_dom (pr2 projs)) (pr1 projs)]
eqargs in u = o ->
eval (Cut' (Var i) (o `ββ Ξ³))
β ret_delay (i β o β¦ Ξ³ β¦) Ξ: neg_ctx i: Ξ β Β¬ (a0 `+ b0) Ξ³: dom (PInl u) =[ val_n ]> Ξ H2: β (a0 `+ b0),' PInl u = (Β¬ (a0 `+ b0)) β ,' PInl u
eval (Cut (Val (Inl (u `α΅₯β Ξ³))) (Var i))
β ret_delay (i β PInl u β¦ Ξ³ β¦)
a1, b1: pre_ty u: pat β b1 H: forall (Ξ : neg_ctx) (A : ty) (i : Ξ β A)
(o : pat A β ) (Ξ³ : dom o =[ val_n ]> Ξ)
(eqargs : {| pr1 := β b1; pr2 := u |} =
{| pr1 := A β ; pr2 := o |}),
rew [funprojs : sigma (funA0 : ty => pat A0) =>
val (pat_dom (pr2 projs)) (pr1 projs)]
eqargs in u = o ->
eval (Cut' (Var i) (o `ββ Ξ³))
β ret_delay (i β o β¦ Ξ³ β¦) Ξ: neg_ctx i: Ξ β Β¬ (a1 `+ b1) Ξ³: dom (PInr u) =[ val_n ]> Ξ H2: β (a1 `+ b1),' PInr u = (Β¬ (a1 `+ b1)) β ,' PInr u
eval (Cut (Val (Inr (u `α΅₯β Ξ³))) (Var i))
β ret_delay (i β PInr u β¦ Ξ³ β¦)
a5, b5: pre_ty v: pat β a5 H: forall (Ξ : neg_ctx) (A : ty) (i : Ξ β A)
(o : pat A β ) (Ξ³ : dom o =[ val_n ]> Ξ)
(eqargs : {| pr1 := β a5; pr2 := v |} =
{| pr1 := A β ; pr2 := o |}),
rew [funprojs : sigma (funA0 : ty => pat A0) =>
val (pat_dom (pr2 projs)) (pr1 projs)]
eqargs in v = o ->
eval (Cut' (Var i) (o `ββ Ξ³))
β ret_delay (i β o β¦ Ξ³ β¦) Ξ: neg_ctx i: Ξ β β (a5 `β b5) Ξ³: dom (PApp v) =[ val_n ]> Ξ H2: Β¬ (a5 `β b5),' PApp v = (β (a5 `β b5)) β ,' PApp v
eval
(Cut (Val (Var i))
(App (v `α΅₯βα΅£ r_pop `α΅₯β Ξ³) (Ξ³ Β¬ b5 Ctx.top)))
β ret_delay (i β PApp v β¦ Ξ³ β¦)
Ξ: neg_ctx i: Ξ β Β¬ `1 Ξ³: dom PTt =[ val_n ]> Ξ H1: β `1,' PTt = (Β¬ `1) β ,' PTt
nf_eq (s_var_upg i β w_split `1 (Ξ³ β `1 Ctx.top))
(i β PTt β¦ Ξ³ β¦)
a, b: pre_ty Ξ: neg_ctx i: Ξ β Β¬ (a `Γ b) Ξ³: dom PPair =[ val_n ]> Ξ H1: β (a `Γ b),' PPair = (Β¬ (a `Γ b)) β ,' PPair
nf_eq
(s_var_upg i
β w_split (a `Γ b) (Ξ³ β (a `Γ b) Ctx.top))
(i β PPair β¦ Ξ³ β¦)
a0, b0: pre_ty u: pat β a0 H: forall (Ξ : neg_ctx) (A : ty) (i : Ξ β A)
(o : pat A β ) (Ξ³ : dom o =[ val_n ]> Ξ)
(eqargs : {| pr1 := β a0; pr2 := u |} =
{| pr1 := A β ; pr2 := o |}),
rew [funprojs : sigma (funA0 : ty => pat A0) =>
val (pat_dom (pr2 projs)) (pr1 projs)]
eqargs in u = o ->
eval (Cut' (Var i) (o `ββ Ξ³))
β ret_delay (i β o β¦ Ξ³ β¦) Ξ: neg_ctx i: Ξ β Β¬ (a0 `+ b0) Ξ³: dom (PInl u) =[ val_n ]> Ξ H2: β (a0 `+ b0),' PInl u = (Β¬ (a0 `+ b0)) β ,' PInl u
nf_eq
(s_var_upg i β w_split (a0 `+ b0) (Inl (u `α΅₯β Ξ³)))
(i β PInl u β¦ Ξ³ β¦)
a1, b1: pre_ty u: pat β b1 H: forall (Ξ : neg_ctx) (A : ty) (i : Ξ β A)
(o : pat A β ) (Ξ³ : dom o =[ val_n ]> Ξ)
(eqargs : {| pr1 := β b1; pr2 := u |} =
{| pr1 := A β ; pr2 := o |}),
rew [funprojs : sigma (funA0 : ty => pat A0) =>
val (pat_dom (pr2 projs)) (pr1 projs)]
eqargs in u = o ->
eval (Cut' (Var i) (o `ββ Ξ³))
β ret_delay (i β o β¦ Ξ³ β¦) Ξ: neg_ctx i: Ξ β Β¬ (a1 `+ b1) Ξ³: dom (PInr u) =[ val_n ]> Ξ H2: β (a1 `+ b1),' PInr u = (Β¬ (a1 `+ b1)) β ,' PInr u
nf_eq
(s_var_upg i β w_split (a1 `+ b1) (Inr (u `α΅₯β Ξ³)))
(i β PInr u β¦ Ξ³ β¦)
nf_eq (snd_nf i (Ξ³ Β¬ b4 Ctx.top)) (i β PSnd β¦ Ξ³ β¦)
a5, b5: pre_ty v: pat β a5 H: forall (Ξ : neg_ctx) (A : ty) (i : Ξ β A)
(o : pat A β ) (Ξ³ : dom o =[ val_n ]> Ξ)
(eqargs : {| pr1 := β a5; pr2 := v |} =
{| pr1 := A β ; pr2 := o |}),
rew [funprojs : sigma (funA0 : ty => pat A0) =>
val (pat_dom (pr2 projs)) (pr1 projs)]
eqargs in v = o ->
eval (Cut' (Var i) (o `ββ Ξ³))
β ret_delay (i β o β¦ Ξ³ β¦) Ξ: neg_ctx i: Ξ β β (a5 `β b5) Ξ³: dom (PApp v) =[ val_n ]> Ξ H2: Β¬ (a5 `β b5),' PApp v = (β (a5 `β b5)) β ,' PApp v
nf_eq (app_nf i (v `α΅₯βα΅£ r_pop `α΅₯β Ξ³) (Ξ³ Β¬ b5 Ctx.top))
(i β PApp v β¦ Ξ³ β¦)
a0, b0: pre_ty u: pat β a0 H: forall (Ξ : neg_ctx) (A : ty) (i : Ξ β A)
(o : pat A β ) (Ξ³ : dom o =[ val_n ]> Ξ)
(eqargs : {| pr1 := β a0; pr2 := u |} =
{| pr1 := A β ; pr2 := o |}),
rew [funprojs : sigma (funA0 : ty => pat A0) =>
val (pat_dom (pr2 projs)) (pr1 projs)]
eqargs in u = o ->
eval (Cut' (Var i) (o `ββ Ξ³))
β ret_delay (i β o β¦ Ξ³ β¦) Ξ: neg_ctx i: Ξ β Β¬ (a0 `+ b0) Ξ³: dom (PInl u) =[ val_n ]> Ξ H2: β (a0 `+ b0),' PInl u = (Β¬ (a0 `+ b0)) β ,' PInl u
nf_eq
(s_var_upg i β w_split (a0 `+ b0) (Inl (u `α΅₯β Ξ³)))
(i β PInl u β¦ Ξ³ β¦)
a1, b1: pre_ty u: pat β b1 H: forall (Ξ : neg_ctx) (A : ty) (i : Ξ β A)
(o : pat A β ) (Ξ³ : dom o =[ val_n ]> Ξ)
(eqargs : {| pr1 := β b1; pr2 := u |} =
{| pr1 := A β ; pr2 := o |}),
rew [funprojs : sigma (funA0 : ty => pat A0) =>
val (pat_dom (pr2 projs)) (pr1 projs)]
eqargs in u = o ->
eval (Cut' (Var i) (o `ββ Ξ³))
β ret_delay (i β o β¦ Ξ³ β¦) Ξ: neg_ctx i: Ξ β Β¬ (a1 `+ b1) Ξ³: dom (PInr u) =[ val_n ]> Ξ H2: β (a1 `+ b1),' PInr u = (Β¬ (a1 `+ b1)) β ,' PInr u
nf_eq
(s_var_upg i β w_split (a1 `+ b1) (Inr (u `α΅₯β Ξ³)))
(i β PInr u β¦ Ξ³ β¦)
a5, b5: pre_ty v: pat β a5 H: forall (Ξ : neg_ctx) (A : ty) (i : Ξ β A)
(o : pat A β ) (Ξ³ : dom o =[ val_n ]> Ξ)
(eqargs : {| pr1 := β a5; pr2 := v |} =
{| pr1 := A β ; pr2 := o |}),
rew [funprojs : sigma (funA0 : ty => pat A0) =>
val (pat_dom (pr2 projs)) (pr1 projs)]
eqargs in v = o ->
eval (Cut' (Var i) (o `ββ Ξ³))
β ret_delay (i β o β¦ Ξ³ β¦) Ξ: neg_ctx i: Ξ β β (a5 `β b5) Ξ³: dom (PApp v) =[ val_n ]> Ξ H2: Β¬ (a5 `β b5),' PApp v = (β (a5 `β b5)) β ,' PApp v
nf_eq (app_nf i (v `α΅₯βα΅£ r_pop `α΅₯β Ξ³) (Ξ³ Β¬ b5 Ctx.top))
(i β PApp v β¦ Ξ³ β¦)
a5, b5: pre_ty v: pat β a5 H: forall (Ξ : neg_ctx) (A : ty) (i : Ξ β A)
(o : pat A β ) (Ξ³ : dom o =[ val_n ]> Ξ)
(eqargs : {| pr1 := β a5; pr2 := v |} =
{| pr1 := A β ; pr2 := o |}),
rew [funprojs : sigma (funA0 : ty => pat A0) =>
val (pat_dom (pr2 projs)) (pr1 projs)]
eqargs in v = o ->
eval (Cut' (Var i) (o `ββ Ξ³))
β ret_delay (i β o β¦ Ξ³ β¦) Ξ: neg_ctx i: Ξ β β (a5 `β b5) Ξ³: dom (PApp v) =[ val_n ]> Ξ H2: Β¬ (a5 `β b5),' PApp v = (β (a5 `β b5)) β ,' PApp v
nf_eq (app_nf i (v `α΅₯βα΅£ r_pop `α΅₯β Ξ³) (Ξ³ Β¬ b5 Ctx.top))
(i β PApp v β¦ Ξ³ β¦)
(* a bit of an ugly case because we didn't write proper generic functions for splitting negative values.. hence knowing this one is an App is getting in our way *)
nf_eq
(i
β PApp (p_of_w a5 (v `α΅₯βα΅£ r_pop `α΅₯β Ξ³))
β¦ p_dom_of_w a5 (v `α΅₯βα΅£ r_pop `α΅₯β Ξ³)
βΆβ Ξ³ Β¬ b5 Ctx.top β¦) (i β PApp v β¦ Ξ³ β¦)
nf_eq
(i
β PApp (p_of_w a5 (v `α΅₯β r_pop α΅£β Ξ³))
β¦ p_dom_of_w a5 (v `α΅₯β r_pop α΅£β Ξ³)
βΆβ Ξ³ Β¬ b5 Ctx.top β¦) (i β PApp v β¦ Ξ³ β¦)
a5, b5: pre_ty v: pat β a5 Ξ: neg_ctx i: Ξ β β (a5 `β b5) Ξ³: dom (PApp v) =[ val_n ]> Ξ Ξ³':= (r_pop α΅£β Ξ³)%asgn: pat_dom v =[ val ]> Ξ
nf_eq
(i
β PApp (p_of_w a5 (v `α΅₯β r_pop α΅£β Ξ³))
β¦ p_dom_of_w a5 (v `α΅₯β r_pop α΅£β Ξ³)
βΆβ Ξ³ Β¬ b5 Ctx.top β¦) (i β PApp v β¦ Ξ³ β¦)
a5, b5: pre_ty v: pat β a5 Ξ: neg_ctx i: Ξ β β (a5 `β b5) Ξ³: dom (PApp v) =[ val_n ]> Ξ Ξ³':= (r_pop α΅£β Ξ³)%asgn: pat_dom v =[ val ]> Ξ
nf_eq
(i
β PApp (p_of_w a5 (v `α΅₯β Ξ³'))
β¦ p_dom_of_w a5 (v `α΅₯β Ξ³') βΆβ Ξ³ Β¬ b5 Ctx.top β¦)
(i β PApp v β¦ Ξ³ β¦)
a5, b5: pre_ty v: pat β a5 Ξ: neg_ctx i: Ξ β β (a5 `β b5) Ξ³: dom (PApp v) =[ val_n ]> Ξ Ξ³':= (r_pop α΅£β Ξ³)%asgn: pat_dom v =[ val ]> Ξ vv:= Ξ³ Β¬ b5 Ctx.top: term Ξ Β¬ b5
nf_eq
(i
β PApp (p_of_w a5 (v `α΅₯β Ξ³'))
β¦ p_dom_of_w a5 (v `α΅₯β Ξ³') βΆβ vv β¦)
(i β PApp v β¦ Ξ³ β¦)
a5, b5: pre_ty v: pat β a5 Ξ: neg_ctx i: Ξ β β (a5 `β b5) Ξ³: dom (PApp v) =[ val_n ]> Ξ Ξ³':= (r_pop α΅£β Ξ³)%asgn: pat_dom v =[ val ]> Ξ vv:= Ξ³ Β¬ b5 Ctx.top: term Ξ Β¬ b5 H: Ξ³' βΆβ upg_k vv β‘β Ξ³
nf_eq
(i
β PApp (p_of_w a5 (v `α΅₯β Ξ³'))
β¦ p_dom_of_w a5 (v `α΅₯β Ξ³') βΆβ vv β¦)
(i β PApp v β¦ Ξ³ β¦)
a5, b5: pre_ty v: pat β a5 Ξ: neg_ctx i: Ξ β β (a5 `β b5) Ξ³: dom (PApp v) =[ val_n ]> Ξ a: pat_dom v =[ val ]> Ξ t: term Ξ Β¬ b5 H: a βΆβ upg_k t β‘β Ξ³
nf_eq
(i
β PApp (p_of_w a5 (v `α΅₯β a))
β¦ p_dom_of_w a5 (v `α΅₯β a) βΆβ t β¦)
(i β PApp v β¦ Ξ³ β¦)
a5, b5: pre_ty v: pat β a5 Ξ: neg_ctx i: Ξ β β (a5 `β b5) Ξ³: dom (PApp v) =[ val_n ]> Ξ a: pat_dom v =[ val ]> Ξ t: term Ξ Β¬ b5 H: a βΆβ upg_k t β‘β Ξ³ H0: rew [funp : pat β a5 => pat_dom p =[ val ]> Ξ]
p_of_w_eq a5 v a in
p_dom_of_w a5 ((v : val (pat_dom v) β a5) `α΅₯β a)
β‘β a
nf_eq
(i
β PApp (p_of_w a5 (v `α΅₯β a))
β¦ p_dom_of_w a5 (v `α΅₯β a) βΆβ t β¦)
(i β PApp v β¦ Ξ³ β¦)
a5, b5: pre_ty v: pat β a5 Ξ: neg_ctx i: Ξ β β (a5 `β b5) Ξ³: dom (PApp v) =[ val_n ]> Ξ a: pat_dom v =[ val ]> Ξ t: term Ξ Β¬ b5 H: a βΆβ upg_k t β‘β Ξ³ H':= p_of_w_eq a5 v a: p_of_w a5 ((v : val (pat_dom v) β a5) `α΅₯β a) = v H0: rew [funp : pat β a5 => pat_dom p =[ val ]> Ξ]
H' in
p_dom_of_w a5 ((v : val (pat_dom v) β a5) `α΅₯β a)
β‘β a
nf_eq
(i
β PApp (p_of_w a5 (v `α΅₯β a))
β¦ p_dom_of_w a5 (v `α΅₯β a) βΆβ t β¦)
(i β PApp v β¦ Ξ³ β¦)
a5, b5: pre_ty v: pat β a5 Ξ: neg_ctx i: Ξ β β (a5 `β b5) Ξ³: dom (PApp v) =[ val_n ]> Ξ a: pat_dom v =[ val ]> Ξ t: term Ξ Β¬ b5 H: a βΆβ upg_k t β‘β Ξ³ H':= p_of_w_eq a5 v a: p_of_w a5 ((v : val (pat_dom v) β a5) `α΅₯β a) = v aa:= p_dom_of_w a5 ((v : val (pat_dom v) β a5) `α΅₯β a): pat_dom
(p_of_w a5 ((v : val (pat_dom v) β a5) `α΅₯β a)) =[
val ]> Ξ H0: rew [funp : pat β a5 => pat_dom p =[ val ]> Ξ]
H' in aa β‘β a
nf_eq (i β PApp (p_of_w a5 (v `α΅₯β a)) β¦ aa βΆβ t β¦)
(i β PApp v β¦ Ξ³ β¦)
a5, b5: pre_ty v: pat β a5 Ξ: neg_ctx i: Ξ β β (a5 `β b5) Ξ³: dom (PApp v) =[ val_n ]> Ξ a: pat_dom v =[ val ]> Ξ t: term Ξ Β¬ b5 H: a βΆβ upg_k t β‘β Ξ³ H':= p_of_w_eq a5 v a: p_of_w a5 ((v : val (pat_dom v) β a5) `α΅₯β a) = v a': pat_dom
(p_of_w a5 ((v : val (pat_dom v) β a5) `α΅₯β a)) =[
val ]> Ξ H0: rew [funp : pat β a5 => pat_dom p =[ val ]> Ξ]
H' in a' β‘β a
nf_eq (i β PApp (p_of_w a5 (v `α΅₯β a)) β¦ a' βΆβ t β¦)
(i β PApp v β¦ Ξ³ β¦)
a5, b5: pre_ty v: pat β a5 Ξ: neg_ctx i: Ξ β β (a5 `β b5) Ξ³: dom (PApp v) =[ val_n ]> Ξ a: pat_dom v =[ val ]> Ξ t: term Ξ Β¬ b5 H: a βΆβ upg_k t β‘β Ξ³ H':= p_of_w_eq a5 v a: p_of_w a5 ((v : val (pat_dom v) β a5) `α΅₯β a) = v a': pat_dom v =[ val ]> Ξ H0: rew [funp : pat β a5 => pat_dom p =[ val ]> Ξ]
eq_refl in a' β‘β a
a' βΆβ t β‘β Ξ³
a5, b5: pre_ty v: pat β a5 Ξ: neg_ctx i: Ξ β β (a5 `β b5) Ξ³: dom (PApp v) =[ val_n ]> Ξ a: pat_dom v =[ val ]> Ξ t: term Ξ Β¬ b5 H: a βΆβ upg_k t β‘β Ξ³ H':= p_of_w_eq a5 v a: p_of_w a5 ((v : val (pat_dom v) β a5) `α΅₯β a) = v a': pat_dom v =[ val ]> Ξ H0: rew [funp : pat β a5 => pat_dom p =[ val ]> Ξ]
eq_refl in a' β‘β a
a' βΆβ t β‘β a βΆβ upg_k t
refine (a_append_eq _ _ _ _ _ _); auto.
well_founded head_inst_nostep
y: ty o: op_copat y B: ty m: op_copat B Ξ: neg_ctx v: val_n Ξ y a: dom o =[ val_n ]> Ξ i: Ξ β B t0: is_var v -> T0 i0: evalβ (v β o β¦ a β¦) β ret_delay (i β m)
Acc head_inst_nostep (B,' m)
p: pre_ty o: op_copat β p B: ty m: op_copat B Ξ: neg_ctx v: val Ξ β p a: dom o =[ val_n ]> Ξ i: Ξ β B t0: is_var v -> T0 i0: evalβ (v β o β¦ a β¦) β ret_delay (i β m)
Acc head_inst_nostep (B,' m)
p: pre_ty o: op_copat Β¬ p B: ty m: op_copat B Ξ: neg_ctx v: val Ξ Β¬ p a: dom o =[ val_n ]> Ξ i: Ξ β B t0: is_var v -> T0 i0: evalβ (v β o β¦ a β¦) β ret_delay (i β m)
Acc head_inst_nostep (B,' m)
A0, B0: pre_ty o: op_copat β (A0 `+ B0) B: ty m: op_copat B Ξ: neg_ctx w: whn Ξ A0 a: dom o =[ val_n ]> Ξ i: Ξ β B t0: is_var (Inl w) -> T0 i0: evalβ (Inl w β o β¦ a β¦) β ret_delay (i β m)
Acc head_inst_nostep (B,' m)
A1, B1: pre_ty o: op_copat β (A1 `+ B1) B: ty m: op_copat B Ξ: neg_ctx w0: whn Ξ B1 a: dom o =[ val_n ]> Ξ i: Ξ β B t0: is_var (Inr w0) -> T0 i0: evalβ (Inr w0 β o β¦ a β¦) β ret_delay (i β m)
Acc head_inst_nostep (B,' m)
o: op_copat β `1 B: ty m: op_copat B Ξ: neg_ctx a: dom o =[ val_n ]> Ξ i: Ξ β B t0: is_var Tt -> T0 i0: evalβ (Tt β o β¦ a β¦) β ret_delay (i β m)
Acc head_inst_nostep (B,' m)
A2, B2: pre_ty o: op_copat β (A2 `Γ B2) B: ty m: op_copat B Ξ: neg_ctx s: state (Ξ βΆβ Β¬ A2) s0: state (Ξ βΆβ Β¬ B2) a: dom o =[ val_n ]> Ξ i: Ξ β B t0: is_var (Pair s s0) -> T0 i0: evalβ (Pair s s0 β o β¦ a β¦) β ret_delay (i β m)
Acc head_inst_nostep (B,' m)
A3, B3: pre_ty o: op_copat β (A3 `β B3) B: ty m: op_copat B Ξ: neg_ctx s1: state (Ξ βΆβ β (A3 `β B3) βΆβ β A3 βΆβ Β¬ B3) a: dom o =[ val_n ]> Ξ i: Ξ β B t0: is_var (Lam s1) -> T0 i0: evalβ (Lam s1 β o β¦ a β¦) β ret_delay (i β m)
Acc head_inst_nostep (B,' m)
A2: pre_ty o: op_copat Β¬ A2 B: ty m: op_copat B Ξ: neg_ctx s0: state (Ξ βΆβ β A2) a: dom o =[ val_n ]> Ξ i: Ξ β B t0: is_var (MuT s0) -> T0 i0: evalβ (MuT s0 β o β¦ a β¦) β ret_delay (i β m)
Acc head_inst_nostep (B,' m)
o: op_copat Β¬ `0 B: ty m: op_copat B Ξ: neg_ctx a: dom o =[ val_n ]> Ξ i: Ξ β B t0: is_var Boom -> T0 i0: evalβ (Boom β o β¦ a β¦) β ret_delay (i β m)
Acc head_inst_nostep (B,' m)
A3, B0: pre_ty o: op_copat Β¬ (A3 `+ B0) B: ty m: op_copat B Ξ: neg_ctx s1: state (Ξ βΆβ β A3) s2: state (Ξ βΆβ β B0) a: dom o =[ val_n ]> Ξ i: Ξ β B t0: is_var (Case s1 s2) -> T0 i0: evalβ (Case s1 s2 β o β¦ a β¦) β ret_delay (i β m)
Acc head_inst_nostep (B,' m)
A4, B1: pre_ty o: op_copat Β¬ (A4 `Γ B1) B: ty m: op_copat B Ξ: neg_ctx t1: term Ξ Β¬ A4 a: dom o =[ val_n ]> Ξ i: Ξ β B t0: is_var (Fst t1) -> T0 i0: evalβ (Fst t1 β o β¦ a β¦) β ret_delay (i β m)
Acc head_inst_nostep (B,' m)
A5, B2: pre_ty o: op_copat Β¬ (A5 `Γ B2) B: ty m: op_copat B Ξ: neg_ctx t2: term Ξ Β¬ B2 a: dom o =[ val_n ]> Ξ i: Ξ β B t0: is_var (Snd t2) -> T0 i0: evalβ (Snd t2 β o β¦ a β¦) β ret_delay (i β m)
Acc head_inst_nostep (B,' m)
A6, B3: pre_ty o: op_copat Β¬ (A6 `β B3) B: ty m: op_copat B Ξ: neg_ctx w0: whn Ξ A6 t3: term Ξ Β¬ B3 a: dom o =[ val_n ]> Ξ i: Ξ β B t0: is_var (App w0 t3) -> T0 i0: evalβ (App w0 t3 β o β¦ a β¦) β ret_delay (i β m)
Acc head_inst_nostep (B,' m)
A0, B0: pre_ty o: op_copat β (A0 `+ B0) B: ty m: op_copat B Ξ: neg_ctx w: whn Ξ A0 a: dom o =[ val_n ]> Ξ i: Ξ β B i0: evalβ (Inl w β o β¦ a β¦) β ret_delay (i β m)
Acc head_inst_nostep (B,' m)
A1, B1: pre_ty o: op_copat β (A1 `+ B1) B: ty m: op_copat B Ξ: neg_ctx w0: whn Ξ B1 a: dom o =[ val_n ]> Ξ i: Ξ β B i0: evalβ (Inr w0 β o β¦ a β¦) β ret_delay (i β m)
Acc head_inst_nostep (B,' m)
o: op_copat β `1 B: ty m: op_copat B Ξ: neg_ctx a: dom o =[ val_n ]> Ξ i: Ξ β B i0: evalβ (Tt β o β¦ a β¦) β ret_delay (i β m)
Acc head_inst_nostep (B,' m)
A2, B2: pre_ty o: op_copat β (A2 `Γ B2) B: ty m: op_copat B Ξ: neg_ctx s: state (Ξ βΆβ Β¬ A2) s0: state (Ξ βΆβ Β¬ B2) a: dom o =[ val_n ]> Ξ i: Ξ β B i0: evalβ (Pair s s0 β o β¦ a β¦) β ret_delay (i β m)
Acc head_inst_nostep (B,' m)
A3, B3: pre_ty o: op_copat β (A3 `β B3) B: ty m: op_copat B Ξ: neg_ctx s1: state (Ξ βΆβ β (A3 `β B3) βΆβ β A3 βΆβ Β¬ B3) a: dom o =[ val_n ]> Ξ i: Ξ β B i0: evalβ (Lam s1 β o β¦ a β¦) β ret_delay (i β m)
Acc head_inst_nostep (B,' m)
A2: pre_ty o: op_copat Β¬ A2 B: ty m: op_copat B Ξ: neg_ctx s0: state (Ξ βΆβ β A2) a: dom o =[ val_n ]> Ξ i: Ξ β B i0: evalβ (MuT s0 β o β¦ a β¦) β ret_delay (i β m)
Acc head_inst_nostep (B,' m)
o: op_copat Β¬ `0 B: ty m: op_copat B Ξ: neg_ctx a: dom o =[ val_n ]> Ξ i: Ξ β B i0: evalβ (Boom β o β¦ a β¦) β ret_delay (i β m)
Acc head_inst_nostep (B,' m)
A3, B0: pre_ty o: op_copat Β¬ (A3 `+ B0) B: ty m: op_copat B Ξ: neg_ctx s1: state (Ξ βΆβ β A3) s2: state (Ξ βΆβ β B0) a: dom o =[ val_n ]> Ξ i: Ξ β B i0: evalβ (Case s1 s2 β o β¦ a β¦) β ret_delay (i β m)
Acc head_inst_nostep (B,' m)
A4, B1: pre_ty o: op_copat Β¬ (A4 `Γ B1) B: ty m: op_copat B Ξ: neg_ctx t1: term Ξ Β¬ A4 a: dom o =[ val_n ]> Ξ i: Ξ β B i0: evalβ (Fst t1 β o β¦ a β¦) β ret_delay (i β m)
Acc head_inst_nostep (B,' m)
A5, B2: pre_ty o: op_copat Β¬ (A5 `Γ B2) B: ty m: op_copat B Ξ: neg_ctx t2: term Ξ Β¬ B2 a: dom o =[ val_n ]> Ξ i: Ξ β B i0: evalβ (Snd t2 β o β¦ a β¦) β ret_delay (i β m)
Acc head_inst_nostep (B,' m)
A6, B3: pre_ty o: op_copat Β¬ (A6 `β B3) B: ty m: op_copat B Ξ: neg_ctx w0: whn Ξ A6 t3: term Ξ Β¬ B3 a: dom o =[ val_n ]> Ξ i: Ξ β B i0: evalβ (App w0 t3 β o β¦ a β¦) β ret_delay (i β m)
Acc head_inst_nostep (B,' m)
a4, b3: pre_ty B: ty m: op_copat B Ξ: neg_ctx s: state (Ξ βΆβ Β¬ a4) s0: state (Ξ βΆβ Β¬ b3) a: dom PFst =[ val_n ]> Ξ i: Ξ β B i0: evalβ
(Cut (Val (Pair s s0)) (Fst (a Β¬ a4 Ctx.top)))
β ret_delay (i β m)
Acc head_inst_nostep (B,' m)
a5, b4: pre_ty B: ty m: op_copat B Ξ: neg_ctx s: state (Ξ βΆβ Β¬ a5) s0: state (Ξ βΆβ Β¬ b4) a: dom PSnd =[ val_n ]> Ξ i: Ξ β B i0: evalβ
(Cut (Val (Pair s s0)) (Snd (a Β¬ b4 Ctx.top)))
β ret_delay (i β m)
Acc head_inst_nostep (B,' m)
a6, b5: pre_ty p1: pat β a6 B: ty m: op_copat B Ξ: neg_ctx s1: state (Ξ βΆβ β (a6 `β b5) βΆβ β a6 βΆβ Β¬ b5) a: dom (PApp p1) =[ val_n ]> Ξ i: Ξ β B i0: evalβ
(Cut (Val (Lam s1))
(App (p1 `α΅₯βα΅£ r_pop `α΅₯β a) (a Β¬ b5 Ctx.top)))
β ret_delay (i β m)
Acc head_inst_nostep (B,' m)
B: ty m: op_copat B Ξ: neg_ctx s0: state (Ξ βΆβ β `1) a: dom PTt =[ val_n ]> Ξ i: Ξ β B i0: evalβ (Cut (Val (a β `1 Ctx.top)) (MuT s0))
β ret_delay (i β m)
Acc head_inst_nostep (B,' m)
a0, b: pre_ty B: ty m: op_copat B Ξ: neg_ctx s0: state (Ξ βΆβ β (a0 `Γ b)) a: dom PPair =[ val_n ]> Ξ i: Ξ β B i0: evalβ
(Cut (Val (a β (a0 `Γ b) Ctx.top)) (MuT s0))
β ret_delay (i β m)
Acc head_inst_nostep (B,' m)
a1, b0: pre_ty p: pat β a1 B: ty m: op_copat B Ξ: neg_ctx s0: state (Ξ βΆβ β (a1 `+ b0)) a: dom (PInl p) =[ val_n ]> Ξ i: Ξ β B i0: evalβ (Cut (Val (Inl (p `α΅₯β a))) (MuT s0))
β ret_delay (i β m)
Acc head_inst_nostep (B,' m)
a2, b1: pre_ty p0: pat β b1 B: ty m: op_copat B Ξ: neg_ctx s0: state (Ξ βΆβ β (a2 `+ b1)) a: dom (PInr p0) =[ val_n ]> Ξ i: Ξ β B i0: evalβ (Cut (Val (Inr (p0 `α΅₯β a))) (MuT s0))
β ret_delay (i β m)
Acc head_inst_nostep (B,' m)
a3, b2: pre_ty B: ty m: op_copat B Ξ: neg_ctx s0: state (Ξ βΆβ β (a3 `β b2)) a: dom PLam =[ val_n ]> Ξ i: Ξ β B i0: evalβ
(Cut (Val (a β (a3 `β b2) Ctx.top)) (MuT s0))
β ret_delay (i β m)
Acc head_inst_nostep (B,' m)
a1, b0: pre_ty p: pat β a1 B: ty m: op_copat B Ξ: neg_ctx s1: state (Ξ βΆβ β a1) s2: state (Ξ βΆβ β b0) a: dom (PInl p) =[ val_n ]> Ξ i: Ξ β B i0: evalβ (Cut (Val (Inl (p `α΅₯β a))) (Case s1 s2))
β ret_delay (i β m)
Acc head_inst_nostep (B,' m)
a2, b1: pre_ty p0: pat β b1 B: ty m: op_copat B Ξ: neg_ctx s1: state (Ξ βΆβ β a2) s2: state (Ξ βΆβ β b1) a: dom (PInr p0) =[ val_n ]> Ξ i: Ξ β B i0: evalβ (Cut (Val (Inr (p0 `α΅₯β a))) (Case s1 s2))
β ret_delay (i β m)
Acc head_inst_nostep (B,' m)
a0, b: pre_ty B: ty m: op_copat B Ξ: neg_ctx t1: term Ξ Β¬ a0 a: dom PPair =[ val_n ]> Ξ i: Ξ β B i0: evalβ
(Cut (Val (a β (a0 `Γ b) Ctx.top)) (Fst t1))
β ret_delay (i β m)
Acc head_inst_nostep (B,' m)
a0, b: pre_ty B: ty m: op_copat B Ξ: neg_ctx t2: term Ξ Β¬ b a: dom PPair =[ val_n ]> Ξ i: Ξ β B i0: evalβ
(Cut (Val (a β (a0 `Γ b) Ctx.top)) (Snd t2))
β ret_delay (i β m)
Acc head_inst_nostep (B,' m)
a3, b2: pre_ty B: ty m: op_copat B Ξ: neg_ctx w0: whn Ξ a3 t3: term Ξ Β¬ b2 a: dom PLam =[ val_n ]> Ξ i: Ξ β B i0: evalβ
(Cut (Val (a β (a3 `β b2) Ctx.top)) (App w0 t3))
β ret_delay (i β m)
Acc head_inst_nostep (B,' m)
a4, b3: pre_ty B: ty m: op_copat B Ξ: neg_ctx s: state (Ξ βΆβ Β¬ a4) s0: state (Ξ βΆβ Β¬ b3) i: Ξ β B v': term Ξ Β¬ a4 i0: evalβ (Cut (Val (Pair s s0)) (Fst v'))
β ret_delay (i β m)
Acc head_inst_nostep (B,' m)
a5, b4: pre_ty B: ty m: op_copat B Ξ: neg_ctx s: state (Ξ βΆβ Β¬ a5) s0: state (Ξ βΆβ Β¬ b4) i: Ξ β B v': term Ξ Β¬ b4 i0: evalβ (Cut (Val (Pair s s0)) (Snd v'))
β ret_delay (i β m)
Acc head_inst_nostep (B,' m)
a6, b5: pre_ty p1: pat β a6 B: ty m: op_copat B Ξ: neg_ctx s1: state (Ξ βΆβ β (a6 `β b5) βΆβ β a6 βΆβ Β¬ b5) a: dom (PApp p1) =[ val_n ]> Ξ i: Ξ β B i0: evalβ
(Cut (Val (Lam s1))
(App (p1 `α΅₯βα΅£ r_pop `α΅₯β a) (a Β¬ b5 Ctx.top)))
β ret_delay (i β m)
Acc head_inst_nostep (B,' m)
B: ty m: op_copat B Ξ: neg_ctx s0: state (Ξ βΆβ β `1) i: Ξ β B v': whn Ξ `1 i0: evalβ (Cut (Val v') (MuT s0)) β ret_delay (i β m)
Acc head_inst_nostep (B,' m)
a0, b: pre_ty B: ty m: op_copat B Ξ: neg_ctx s0: state (Ξ βΆβ β (a0 `Γ b)) i: Ξ β B v': whn Ξ (a0 `Γ b) i0: evalβ (Cut (Val v') (MuT s0)) β ret_delay (i β m)
Acc head_inst_nostep (B,' m)
a1, b0: pre_ty p: pat β a1 B: ty m: op_copat B Ξ: neg_ctx s0: state (Ξ βΆβ β (a1 `+ b0)) a: dom (PInl p) =[ val_n ]> Ξ i: Ξ β B i0: evalβ (Cut (Val (Inl (p `α΅₯β a))) (MuT s0))
β ret_delay (i β m)
Acc head_inst_nostep (B,' m)
a2, b1: pre_ty p0: pat β b1 B: ty m: op_copat B Ξ: neg_ctx s0: state (Ξ βΆβ β (a2 `+ b1)) a: dom (PInr p0) =[ val_n ]> Ξ i: Ξ β B i0: evalβ (Cut (Val (Inr (p0 `α΅₯β a))) (MuT s0))
β ret_delay (i β m)
Acc head_inst_nostep (B,' m)
a3, b2: pre_ty B: ty m: op_copat B Ξ: neg_ctx s0: state (Ξ βΆβ β (a3 `β b2)) i: Ξ β B v': whn Ξ (a3 `β b2) i0: evalβ (Cut (Val v') (MuT s0)) β ret_delay (i β m)
Acc head_inst_nostep (B,' m)
a1, b0: pre_ty p: pat β a1 B: ty m: op_copat B Ξ: neg_ctx s1: state (Ξ βΆβ β a1) s2: state (Ξ βΆβ β b0) a: dom (PInl p) =[ val_n ]> Ξ i: Ξ β B i0: evalβ (Cut (Val (Inl (p `α΅₯β a))) (Case s1 s2))
β ret_delay (i β m)
Acc head_inst_nostep (B,' m)
a2, b1: pre_ty p0: pat β b1 B: ty m: op_copat B Ξ: neg_ctx s1: state (Ξ βΆβ β a2) s2: state (Ξ βΆβ β b1) a: dom (PInr p0) =[ val_n ]> Ξ i: Ξ β B i0: evalβ (Cut (Val (Inr (p0 `α΅₯β a))) (Case s1 s2))
β ret_delay (i β m)
Acc head_inst_nostep (B,' m)
a0, b: pre_ty B: ty m: op_copat B Ξ: neg_ctx t1: term Ξ Β¬ a0 i: Ξ β B v': whn Ξ (a0 `Γ b) i0: evalβ (Cut (Val v') (Fst t1)) β ret_delay (i β m)
Acc head_inst_nostep (B,' m)
a0, b: pre_ty B: ty m: op_copat B Ξ: neg_ctx t2: term Ξ Β¬ b i: Ξ β B v': whn Ξ (a0 `Γ b) i0: evalβ (Cut (Val v') (Snd t2)) β ret_delay (i β m)
Acc head_inst_nostep (B,' m)
a3, b2: pre_ty B: ty m: op_copat B Ξ: neg_ctx w0: whn Ξ a3 t3: term Ξ Β¬ b2 i: Ξ β B v': whn Ξ (a3 `β b2) i0: evalβ (Cut (Val v') (App w0 t3))
β ret_delay (i β m)
Acc head_inst_nostep (B,' m)
a0, b: pre_ty B: ty m: op_copat B Ξ: neg_ctx t1: term Ξ Β¬ a0 i: Ξ β B v': whn Ξ (a0 `Γ b) i0: evalβ (Cut (Val v') (Fst t1)) β ret_delay (i β m)
Acc head_inst_nostep (B,' m)
a0, b: pre_ty B: ty m: op_copat B Ξ: neg_ctx t2: term Ξ Β¬ b i: Ξ β B v': whn Ξ (a0 `Γ b) i0: evalβ (Cut (Val v') (Snd t2)) β ret_delay (i β m)
Acc head_inst_nostep (B,' m)
a3, b2: pre_ty B: ty m: op_copat B Ξ: neg_ctx w0: whn Ξ a3 t3: term Ξ Β¬ b2 i: Ξ β B v': whn Ξ (a3 `β b2) i0: evalβ (Cut (Val v') (App w0 t3))
β ret_delay (i β m)
Acc head_inst_nostep (B,' m)
a0, b: pre_ty B: ty m: op_copat B Ξ: neg_ctx t1: term Ξ Β¬ a0 i: Ξ β B c: Ξ β β (a0 `Γ b) i0: evalβ (Cut (Val (VarL c)) (Fst t1))
β ret_delay (i β m)
Acc head_inst_nostep (B,' m)
a0, b: pre_ty B: ty m: op_copat B Ξ: neg_ctx t2: term Ξ Β¬ b i: Ξ β B c: Ξ β β (a0 `Γ b) i0: evalβ (Cut (Val (VarL c)) (Snd t2))
β ret_delay (i β m)
Acc head_inst_nostep (B,' m)
a3, b2: pre_ty B: ty m: op_copat B Ξ: neg_ctx w0: whn Ξ a3 t3: term Ξ Β¬ b2 i: Ξ β B c: Ξ β β (a3 `β b2) i0: evalβ (Cut (Val (VarL c)) (App w0 t3))
β ret_delay (i β m)
Acc head_inst_nostep (B,' m)
a0, b: pre_ty Ξ: neg_ctx t1: term Ξ Β¬ a0 c: Ξ β β (a0 `Γ b)
Acc head_inst_nostep (β (a0 `Γ b),' PFst)
a0, b: pre_ty Ξ: neg_ctx t2: term Ξ Β¬ b c: Ξ β β (a0 `Γ b)