proposition: Lemma simpl_env_demo : forall (x y:atom) (T1 T2:typ) (E F:env), ((x ~ T1) ++ nil) ++ (y,T2) :: (nil ++ E) ++ F = (x ~ T1) ++ (y ~ T2) ++ E ++ F.
proof: Proof. intros. simpl_env. reflexivity. Qed.
imports: Metalib.Metatheory String