proposition: Lemma strip_O : forall v : list A, strip v 0 = v.
proof: Proof. intro. unfold strip in |- *. rewrite <- minus_n_O. rewrite <- length_rev. rewrite trunc_all. rewrite rev_rev. trivial with arith. Qed.
imports: Arith_compl Minus Lists_compl