proposition: Theorem progress: forall a t, nil ⊢ a ∈ t -> isvalue a \/ exists a', red a a'.
proof: Proof. intros a t TY; dependent induction TY. - left; apply V_Abs. - destruct IHTY1 as [ISVAL1 | (a1' & RED1)]; auto. + destruct IHTY2 as [ISVAL2 | (a2' & RED2)]; auto. * destruct (canonical_forms a1 (Fun t t')) as (x & a & E); auto. subst a1. right; exists (subst a x a2). apply red_beta; auto. * right; exists (App a1 a2'). apply red_app_2; auto. + right; exists (App a1' a2). apply red_app_1; auto. - left; apply V_Const. - destruct IHTY1 as [ISVAL1 | (a' & RED1)]; auto. + destruct (canonical_forms a Bool) as (b & E); auto. subst a. right; exists (if b then ifso else ifnot). apply red_cond. + right; exists (Cond a' ifso ifnot). apply red_cond_1; auto. Qed.
imports: Coq(Bool String List Program.Equality) CDF(Sequences)