proposition: Theorem well_typed_programs_do_not_go_wrong: forall a t, nil ⊢ a ∈ t -> ~ goes_wrong a.
proof: Proof. intros a t TY (a' & REDS & IRRED & NOTVAL). assert (TY': nil ⊢ a' ∈ t). { clear IRRED NOTVAL. revert a a' REDS TY. induction 1; eauto using reduction_preserves_typing. } destruct (progress a' t TY') as [ISVAL | (a'' & RED)]. - apply NOTVAL. auto. - apply IRRED with a''. auto. Qed.
imports: Coq(Bool String List Program.Equality) CDF(Sequences)