proposition: Lemma freeVarPlus (x y : Term) : freeVarT (Plus x y) = freeVarT x ++ freeVarT y.
proof: Proof. now rewrite <- (app_nil_r (freeVarT y)). Qed.
imports: Coq(Arith Ensembles List) LibHyps(LibHyps) hydras(MoreLibHyps NewNotations)