proposition: Lemma length_a : forall a b n v, t2_length a < t2_length (gcons a b n v).
proof: Proof. simpl; intros; apply Compat815.le_lt_n_Sm. match goal with [ |- ?a <= ?b + ?c + ?d] => rewrite (Nat.add_comm (b + c) d) end. lia. Qed.
imports: Coq(Arith Compare_dec Relations Wellfounded Lia) hydras(More_Arith Restriction T1 OrdNotations Compat815)