proposition: Theorem llist_injection_inj {A:Type}: injective _ _ (llist_injection (A:=A)).
proof: Proof. unfold injective in |- *. - simple induction x; simpl in |- *. simple destruct y; simpl in |- *; [ auto | discriminate 1 ]. intros a l Hl y; case y; simpl in |- *. + discriminate 1. + injection 1; intros e1 e2; rewrite e2; rewrite (Hl _ e1); trivial. Qed.
imports: List Image