proposition: Theorem strong_progress {τ} (e : Exp [] τ) : ValueP e ∨ ∃ e', e ---> e'.
proof: Proof. dependent induction e; reduce. - now left; constructor. - destruct IHe1 as [V1|[e1' H1']]; destruct IHe2 as [V2|[e2' H2']]. + now left; constructor. + dependent elimination H2'; now eauto 6. + dependent elimination H1'; now eauto 6. + dependent elimination H1'; dependent elimination H2'; now eauto 6. - destruct IHe as [V|[e' H']]. + dependent elimination V; now eauto 6. + dependent elimination H'; now eauto 6. - destruct IHe as [V|[e' H']]. + dependent elimination V; now eauto 6. + dependent elimination H'; now eauto 6. - now inv v. - now left; constructor. - right. destruct IHe1 as [V1|[e1' H1']]; destruct IHe2 as [V2|[e2' H2']]. + dependent elimination V1; now eauto 6. + dependent elimination H2'; now eauto 6. + dependent elimination H1'; now eauto 6. + dependent elimination H1'; now eauto 6. Qed.
imports: Coq.Lists.List Category.Lib Category.Instance.Lambda.Ltac Category.Instance.Lambda.Ty Category.Instance.Lambda.Exp Category.Instance.Lambda.Value Category.Instance.Lambda.Sub Equations(Equations)