proposition: Lemma length_abnc : forall a b n c, t2_length a + t2_length b <= t2_length (gcons a b n c).
proof: Proof. intros; eapply Nat.le_trans. - eapply length_ab. - apply length_psi. Qed.
imports: Coq(Arith Compare_dec Relations Wellfounded Lia) hydras(More_Arith Restriction T1 OrdNotations Compat815)