proposition: Lemma injection_demo : forall (A:Set)(a b : A)(l l': LList A), LCons a (LCons b l) = LCons b (LCons a l') -> a = b /\ l = l'.
proof: Proof. intros A a b l l' e; injection e; auto. Qed.
imports: Arith Vector List Extraction ZArith Compare_dec ZArith List Wf_nat Bool