proposition: Lemma cons_cons_inv : forall (x1 x2 : Elt) (w1 w2 : Word), cons x1 w1 = cons x2 w2 -> x1 = x2 /\ w1 = w2.
proof: Proof. intros. split. replace x1 with (fun_consaw_a (cons x1 w1)); auto. replace x2 with (fun_consaw_a (cons x2 w2)); auto. apply (f_equal (A:=Word) (B:=Elt)); auto. replace w1 with (fun_consaw_w (cons x1 w1)); auto. replace w2 with (fun_consaw_w (cons x2 w2)); auto. apply (f_equal (A:=Word) (B:=Word)); auto. Qed.
imports: Ensf