proposition: Lemma filter_weak_cont_closed : reflexive succ -> context_closed succ -> context_closed fsucc.
proof: Proof. rewrite <- !Vmonotone_context_closed. unfold Vmonotone, Vmonotone_i, RelUtil.monotone. intros hrefl hcc f i j e vi vj. unfold fsucc. simpl. intros t u. set (t' := filter t). set (u' := filter u). intro h'. rewrite !Vmap_cast, !Vmap_app. simpl. fold t' u'. set (vi' := Vmap filter vi). set (vj' := Vmap filter vj). set (vt := Vcast (Vapp vi' (Vcons t' vj')) e). set (vu := Vcast (Vapp vi' (Vcons u' vj')) e). case (In_dec eq_nat_dec i (map N_val (pi f))); intro Hi. destruct (in_map_elim Hi) as [x [hx vx]]. destruct (in_elim hx) as [l1 [l2 hf]]. assert (a: length l1+length(x::l2)=@arity Sig' f). unfold arity, filter_sig, filter_arity. rewrite hf, length_app. refl. rewrite (Vfilter_app_eq (v:=vt) a hf), (Vfilter_app_eq (v:=vu) a hf). simpl. ded (hyp f). unfold non_dup in H. rewrite hf, map_app in H. simpl in H. destruct (nodup_app_cons H) as [h1 h2]. rewrite <- vx in h1. rewrite <- vx in h2. assert (e1 : Vfilter l1 vt = Vfilter l1 vu). apply Vfilter_eq_notin. intros hi h. ded (in_map N_val h). contr. rewrite e1. assert (e2 : Vfilter l2 vt = Vfilter l2 vu). apply Vfilter_eq_notin. intros hi h. ded (in_map N_val h). contr. rewrite e2. apply hcc. unfold vt, vu. rewrite !Vnth_cast, !Vnth_app. destruct (le_gt_dec i x). 2: lia. repeat (rewrite Vnth_cons_head; [idtac|rewrite vx;lia]). hyp. apply eq_incl_refl_rel. hyp. apply args_eq. unfold vt, vu. apply Vfilter_eq_notin with (l:=pi f). intros hi h. ded (in_map N_val h). contr. Qed.
imports: CoLoR(LogicUtil ATrs ListUtil NatUtil VecUtil SN BoolUtil RelUtil ListNodup VecFilterPerm ARelation ACompat NaryFunction BoundNat ListDec)