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