proposition: Theorem well_typed_programs_are_safe: forall a t, nil ⊢ a ∈ t -> safe a.
proof: Proof. cofix CIH; intros. destruct (progress a t H) as [ISVAL | (a' & RED)]. - apply safe_value; auto. - apply safe_red with a'; auto. apply CIH with t. apply reduction_preserves_typing with a; auto. Qed.
imports: Coq(Bool String List Program.Equality) CDF(Sequences)