proposition: Lemma pow3Min : forall a : nat, 1 <= pow3 a.
proof: Proof. induction a as [| a Hreca]. - apply le_n. - simpl; eapply Nat.le_trans. + apply Hreca. + apply Nat.le_add_r. Qed.
imports: Coq(Arith Vector Lia) hydras.Ackermann(primRec cPair folProp code extEqualNat codeSubTerm codeFreeVar)