proposition: Lemma rev_eq : forall A, @List.rev A = @LibList.rev A.
proof: Proof. Proof using. extens ;=> L. induction L; simpl; rew_list. { auto. } { rewrite IHL. rewrite <- app_eq. unfold app. fequals. } Qed.
imports: TLC(LibTactics LibReflect)