(* *)
(**************************************************************************)
-include "ground_2/notation/constructors/nil_0.ma".
+include "ground_2/notation/constructors/circledE_1.ma".
include "ground_2/notation/constructors/oplusright_3.ma".
include "ground_2/lib/arith.ma".
| nil : list A
| cons: A → list A → list A.
-interpretation "nil (list)" 'Nil = (nil ?).
+interpretation "nil (list)" 'CircledE A = (nil A).
interpretation "cons (list)" 'OPlusRight A hd tl = (cons A hd tl).
(* Basic inversion lemmas on length *****************************************)
-lemma length_inv_zero_dx (A:Type[0]) (l:list A): |l| = 0 â\86\92 l = â\97\8a.
+lemma length_inv_zero_dx (A:Type[0]) (l:list A): |l| = 0 â\86\92 l = â\92º.
#A * // #a #l >length_cons #H destruct
qed-.
-lemma length_inv_zero_sn (A:Type[0]) (l:list A): 0 = |l| â\86\92 l = â\97\8a.
+lemma length_inv_zero_sn (A:Type[0]) (l:list A): 0 = |l| â\86\92 l = â\92º.
/2 width=1 by length_inv_zero_dx/ qed-.
lemma length_inv_succ_dx (A:Type[0]) (l:list A) (x): |l| = ↑x →