proposition: Lemma closedNN1 : ClosedSystem LNN NN.
proof: Proof. intros v f H; repeat induction H; cbn; auto. Qed.
imports: Coq(Arith Lia Ensembles List) hydras.Ackermann(folProp subAll folLogic3 Languages) hydras(Compat815 NewNotations)