proposition: Lemma simpl_env_demo : forall (x y:atom) (T1 T2:typ) (E F:ctx), ([(x, T1)] ++ nil) ++ (y,T2) :: (nil ++ E) ++ F = [(x,T1)] ++ [(y, T2)] ++ E ++ F.
proof: Proof. intros. simpl_env. reflexivity. Qed.
imports: String Metalib.Metatheory Stlc.Definitions Stlc.Lemmas Stlc.Lec1