proposition: Lemma weakening: forall E a t, E ⊢ a ∈ t -> forall E', (forall x tx, lookup x E = Some tx -> lookup x E' = Some tx) -> E' ⊢ a ∈ t.
proof: Proof. induction 1; intros E' W; eauto using has_type. - apply T_Abs. apply IHhas_type. cbn; intros. destruct (string_dec x0 x); auto. Qed.
imports: Coq(Bool String List Program.Equality) CDF(Sequences)