proposition: Theorem reduction_preserves_typing: forall a a', red a a' -> forall t, nil ⊢ a ∈ t -> nil ⊢ a' ∈ t.
proof: Proof. induction 1; intros t TY. - inversion TY; subst. inversion H3; subst. eapply substitution_preserves_typing; eauto. cbn. destruct (string_dec x x); congruence. cbn; intros. destruct (string_dec y x); congruence. - inversion TY; subst. destruct b; auto. - inversion TY; subst. apply T_App with t0; eauto. - inversion TY; subst. apply T_App with t0; eauto. - inversion TY; subst. apply T_Cond; eauto. Qed.
imports: Coq(Bool String List Program.Equality) CDF(Sequences)