proposition: Lemma G_forward m: Grel m (m * n) (T m).
proof: Proof. unfold Grel. asimpl. do 2 eapply equiv_lam_proper. unfold Cons at 2. rewrite G_left_reduce, G_right_reduce. rewrite <-lin_cons. change (⟨ A, B ⟩) with (t 0). rewrite <-tab_S. change (_ ::: _) with (lin [t m] Nil). now rewrite <-lin_app. 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