proposition: Lemma filter_weak_cont_closed : weak_context_closed succ succ_eq -> weak_context_closed fsucc fsucc_eq.
proof: Proof. intro. unfold weak_context_closed. intros. assert (clos_refl fsucc t1 t2). unfold clos_refl, union. auto. ded (rc_filter_ord H1). assert (context_closed fsucc_eq). apply filter_cont_closed. apply rc_refl. apply rc_context_closed. hyp. apply H3. hyp. Qed.
imports: CoLoR(ATrs VecFilter VecUtil LogicUtil RelUtil SN NatUtil ARelation ACompat) Coq(List)