proposition: Lemma G_right_reduce m: (T m) Nil (enc n A) (Succ B) ≡ lin (tab (S >> t) m) Nil.
proof: Proof. rewrite G_right_subst. asimpl. eapply eq_equiv. f_equal. rewrite tab_map. eapply tab_ext. intros ?; unfold funcomp, t; cbn; asimpl. unfold Pair, τ; cbn. f_equal. f_equal. rewrite <-enc_app. f_equal; lia. now simplify. 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