proposition: Lemma G_backward_exists m p M: normal M -> Grel m p M -> exists l, M = T l.
proof: Proof. intros N [M' [-> [l ->] % steps_u]] % multiplication_lambdas; auto. exists l; erewrite tab_ext; now eauto. 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