proposition: Lemma filter_cont_true : filter (fill (Cont f e v1 c v2) t) = fill (Cont' f e_true v1' Hole v2') t'.
proof: Proof. simpl. rewrite Vmap_cast, Vmap_app. simpl. rewrite Vfilter_cast, Vfilter_app, Vcast_cast. fold bs t' v1'. assert (Vfilter (snd bs) (Vcons t' (Vmap filter v2)) = Vcast (Vcons t' v2') (Vtrue_Sn_true (snd bs) H)). rewrite (Vfilter_head_true t' (Vmap filter v2) H). refl. rewrite H0, Vapp_rcast, Vcast_cast. refl. Qed.
imports: CoLoR(ATrs VecFilter VecUtil LogicUtil RelUtil SN NatUtil ARelation ACompat) Coq(List)