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) hydras.Ackermann(Languages folProof folProp folLogic3)