proposition: Lemma In_add2 {T:Type}(a b:T)(S : Ensemble T): In S a -> In (Add S b) a.
proof: Proof. left; auto with sets. Qed.
imports: Coq(Arith Lists.List) hydras.Ackermann(fol folProp folProof Languages folLogic folLogic2 folLogic3 subAll Deduction primRec)