proposition: Lemma L6: RepresentableHalf1 NN 2 (fun n p => p) (v#0 = v#1)%fol.
proof: Proof. intros a b; simpl. unfold substF; simpl. Search substT . apply impRefl. Qed.
imports: hydras.Ackermann(expressible) hydras.Ackermann(NN NewNotations NNtheory) Coq(Lia)