proposition: Lemma substitution_preserves_typing: forall E a t, E ⊢ a ∈ t -> forall x c t' E', nil ⊢ c ∈ t' -> lookup x E = Some t' -> (forall y ty, y <> x -> lookup y E = Some ty -> lookup y E' = Some ty) -> E' ⊢ subst a x c ∈ t.
proof: Proof. induction 1; intros until E'; intros TYC TYX TYE; cbn. - destruct (string_dec x0 x). + replace t with t' by congruence. apply weakening with (E := nil); auto. cbn; intros; discriminate. + apply T_Var. apply TYE; auto. - destruct (string_dec x0 x). + subst x0. apply T_Abs. apply weakening with (E := (x, t) :: E); auto. cbn; intros. destruct (string_dec x0 x); auto. + apply T_Abs. eapply IHhas_type; eauto. cbn. destruct (string_dec x0 x); congruence. cbn; intros. destruct (string_dec y x); auto. - apply T_App with t; eauto. - apply T_Const. - apply T_Cond; eauto. Qed.
imports: Coq(Bool String List Program.Equality) CDF(Sequences)