proposition: Lemma L5: RepresentableHalf1 NN 2 (fun n p => n) (v#0 = v#2)%fol.
proof: Proof. intros a b; simpl. unfold substF; simpl. Search substT . rewrite subProp.subTermNil. Search (SysPrf _ (?A -> ?A)%fol). apply impRefl. induction a. simpl. tauto. simpl. simpl. Search freeVarT (S_ _). now rewrite freeVarSucc. Qed.
imports: hydras.Ackermann(expressible) hydras.Ackermann(NN NewNotations NNtheory) Coq(Lia)