proposition: Lemma length_psi : forall a b n c, t2_length [a, b] <= t2_length (gcons a b n c).
proof: Proof. simpl; intros; apply Compat815.le_lt_n_Sm ; lia. Qed.
imports: Coq(Arith Compare_dec Relations Wellfounded Lia) hydras(More_Arith Restriction T1 OrdNotations Compat815)