proposition: Lemma remove_length_eq_S {A R} {_ : @Equivalence A R} (dec : forall x y, {R x y} + {~R x y}) (ls ls' : list A) x (H0 : InA R x ls) (H1 : ~InA R x ls') (Hls : NoDupA R ls) (Hls' : NoDupA R ls') (H2 : forall y, (InA R y ls /\ ~R y x) <-> InA R y ls') : List.length ls = S (List.length ls').
proof: Proof. rewrite <- (@removeA_length_In _ R _ _ dec x ls) by assumption. apply f_equal, equivlist_length; try assumption. { apply removeA_NoDupA; assumption. } { intro y; specialize (H2 y); rewrite <- H2; clear H2. rewrite removeA_InA by assumption. intuition. } Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Coq.Lists.List Coq.Lists.SetoidList Coq.Bool.Bool Fiat.Common Fiat.Common.List.Operations Fiat.Common.Equality Fiat.Common.List.FlattenList Fiat.Common.LogicFacts