1)I have hypothesis that a exists in l . I should write it as (In a l or List.In a l)?
2) During induction i get In a .This is wrong statement in the presence of hypothesis
(In a l). How to prove it wrong?
1) They are the same
Require Import List. Import ListNotations. Locate In. Check In. Check List.In. Check Lists.List.In. Check Coq.Lists.List.In.
2) There is a theorem
Require Import List. Import ListNotations. Check in_nil. Goal forall (a : nat) (P : Prop), In a  -> P. Proof. intros a P H. Check (@in_nil _ a). destruct (@in_nil _ a). exact H. Qed.
Last updated: Oct 04 2023 at 23:01 UTC