proposition: Lemma G_backward_equations m p l: Grel m p (T l) -> m = l /\ m * n = p.
proof: Proof. unfold Grel. rewrite <-G_forward. rewrite !T_ren. rewrite !G_left_reduce. intros H % equiv_lam_elim % equiv_lam_elim. eapply equiv_unique_normal_forms in H; [|auto| |]. eapply lin_injective in H as [_ H]; auto. eapply Cons_injective in H as [[H1 H2] % Pair_injective _]. eapply eq_equiv, enc_injective in H1; auto. eapply eq_equiv, enc_injective in H2; auto. intuition; subst; lia. all: eapply lin_normal. 1, 3: rewrite tab_map_nats; intros; mapinj; unfold t; cbn. all: repeat eapply normal_app_intro; auto. all: now unfold Nil. 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