proposition: Lemma G_iff m p G: normal G -> ((m * n = p /\ G = T m) <-> Grel m p G).
proof: Proof. intros N. split. - intros [<- ->]. apply G_forward. - intros H. specialize (G_backward_exists N H) as [l ->]. eapply G_backward_equations in H; intuition auto. Qed.
imports: List Lia Program.Program Undecidability.HOU(std.std axioms) RelationClasses Morphisms Init.Wf Init.Nat Setoid Undecidability.HOU(calculus.calculus second_order.goldfarb.encoding) FinFun Coq.Arith.Wf_nat