proposition: Lemma length_b : forall a b n v, t2_length b < t2_length (gcons a b n v).
proof: Proof. simpl; lia. Qed.
imports: Coq(Arith Compare_dec Relations Wellfounded Lia) hydras(More_Arith Restriction T1 OrdNotations Compat815)