proposition: Lemma filter_cont_closed : reflexive succ -> context_closed succ -> context_closed fsucc.
proof: Proof. intros Hrefl H. unfold context_closed, filter_ord. induction c; intros. simpl. hyp. set (bs := Vbreak (n1:=i) (n2:=S j) (Vcast (pi f) (sym_eq e))). case_eq (Vhead (snd bs)); intro H1. rewrite (filter_cont_true e t c t0 t1 H1). rewrite (filter_cont_true e t c t0 t2 H1). apply H. apply IHc. hyp. rewrite (filter_cont_false e t c t0 t1 H1). rewrite (filter_cont_false e t c t0 t2 H1). apply Hrefl. Qed.
imports: CoLoR(ATrs VecFilter VecUtil LogicUtil RelUtil SN NatUtil ARelation ACompat) Coq(List)