proposition: Lemma SubExp_SN {Γ Γ'} (env : Sub Γ' Γ) {τ} (e : Exp Γ τ) : SN_Sub env → SN (SubExp env e).
proof: Proof. generalize dependent env. induction e; intros; simpl. - now eexists; repeat constructor. - split. + destruct (SN_halts (IHe1 env X)) as [v1 [P1 Q1]]. destruct (SN_halts (IHe2 env X)) as [v2 [P2 Q2]]. exists (Pair v1 v2). split. * now apply multistep_Pair. * now repeat constructor. + split. * destruct (SN_halts (IHe1 env X)) as [v1 [P1 Q1]]. destruct (SN_halts (IHe2 env X)) as [v2 [P2 Q2]]. apply (multistep_preserves_SN' (e':=v1)); auto. ** rewrite (multistep_Fst1 (p':=Pair v1 v2)). *** now apply multi_R; eauto. *** erewrite multistep_Pair1; eauto. erewrite multistep_Pair2; eauto. now apply multi_refl. ** apply (multistep_preserves_SN (e:=SubExp env e1)); now intuition. * destruct (SN_halts (IHe1 env X)) as [v1 [P1 Q1]]. destruct (SN_halts (IHe2 env X)) as [v2 [P2 Q2]]. apply (multistep_preserves_SN' (e':=v2)); auto. ** rewrite (multistep_Snd1 (p':=Pair v1 v2)). *** now apply multi_R; eauto. *** erewrite multistep_Pair1; eauto. erewrite multistep_Pair2; eauto. now apply multi_refl. ** apply (multistep_preserves_SN (e:=SubExp env e2)); now intuition. - now apply IHe. - now apply IHe. - induction env. + now inv v. + dependent elimination X. now dependent elimination v; simpl in *; simp SubVar. - split. + now eexists; repeat constructor. + intros. destruct (SN_halts X0) as [v [P Q]]. apply (multistep_preserves_SN' (e':=SubExp (Push v env) e)); auto. * eapply multi_trans; eauto. ** now eapply multistep_AppR; eauto. ** apply multi_R; auto. now rewrite SubExp_Push; eauto 6. * apply IHe. constructor; auto. now eapply multistep_preserves_SN; eauto. - now apply IHe1, IHe2. Qed.
imports: Category.Lib Category.Instance.Lambda.Ltac Category.Instance.Lambda.Ty Category.Instance.Lambda.Exp Category.Instance.Lambda.Value Category.Instance.Lambda.Ren Category.Instance.Lambda.Sub Category.Instance.Lambda.Log Category.Instance.Lambda.Sem Category.Instance.Lambda.Multi Category.Instance.Lambda.Sound Category.Instance.Lambda.Step Equations(Equations)