inlist_filter@{u v k | u <= k, v <= k} {A : Type@{u}} (l : list A) (P : A -> Type@{v}) (dec : forall x, Decidable (P x)) (x : A) : iff@{u k k} (InList x (list_filter l P dec)) (InList x l /\ P x). Proof. simple_list_induction l a l IHl. - simpl. apply iff_inverse. apply iff_equiv. snrapply prod_empty_l@{v}. - simpl. nrapply iff_compose. 2: { apply iff_inverse. apply iff_equiv. exact (sum_distrib_r@{k k k _ _ _ k k} _ _ _). } destruct (dec a) as [p|p]. + simpl. snrapply iff_compose. 1: exact (sum (a = x) (prod (InList@{u} x l) (P x))). 1: split; apply functor_sum; only 1,3: exact idmap; apply IHl. split; apply functor_sum@{k k k k}; only 2,4: apply idmap. * intros []. exact (idpath, p). * exact fst. + nrapply iff_compose. 1: apply IHl. apply iff_inverse. apply iff_equiv. nrefine (equiv_compose'@{k k k} (sum_empty_l@{k} _) _). snrapply equiv_functor_sum'@{k k k k k k}. 2: exact equiv_idmap. apply equiv_to_empty. by intros [[] r]. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum