proposition: Lemma in_countIn : forall a a' l, In a l -> eqA a a' -> countIn a' l > 0.
proof: Proof. induction l; inversion 1; intro; simpl. rewrite H0; destruct (eqA_dec a' a). lia. absurd (eqA a' a); intuition. destruct (eqA_dec a' a0). lia. apply IHl; trivial. Qed.
imports: Coq(Permutation Setoid) CoLoR(NatUtil LogicUtil)