proposition: Lemma append_assoc_demo : forall (E0 E1 E2 E3:ctx), E0 ++ (E1 ++ E2) ++ E3 = E0 ++ E1 ++ E2 ++ E3.
proof: Proof. intros. auto. simpl_env. reflexivity. Qed.
imports: String Metalib.Metatheory Stlc.Definitions Stlc.Lemmas Stlc.Lec1