-let rec length2 (A1,A2:Type[0]) (l:list2 A1 A2) on l ≝ match l with
-[ nil2 ⇒ 0
-| cons2 _ _ l ⇒ length2 A1 A2 l + 1
-].
+lemma length_inv_zero_sn (A:Type[0]) (l:list A): 0 = |l| → l = Ⓔ.
+/2 width=1 by length_inv_zero_dx/ qed-.
+
+lemma length_inv_succ_dx (A:Type[0]) (l:list A) (x): |l| = ↑x →
+ ∃∃tl,a. x = |tl| & l = a ⨮ tl.
+#A * /2 width=4 by ex2_2_intro/
+>length_nil #x #H destruct
+qed-.