proposition: Lemma ReplaceTermTermMonotone : forall a s1 s2 : nat, s1 <= s2 -> ReplaceTermTerm a s1 <= ReplaceTermTerm a s2.
proof: Proof. intros; eapply proj1; now apply ReplaceTermTermsTermMonotone. Qed.
imports: Coq(Arith Vector Lia) hydras.Ackermann(primRec cPair folProp code extEqualNat codeSubTerm codeFreeVar)