proposition: Lemma WF_co_scc : forall (hypD : rules_preserve_vars D) ci, incl ci D -> co_scc ci = true -> WF (hd_red_Mod S ci).
proof: Proof. unfold WF. intros. apply SN_intro. intros. apply SN_intro. intros. assert (h : rules_preserve_vars ci). eapply rules_preserve_vars_incl. apply H. hyp. destruct (hd_red_Mod2_hd_rules_graph h H1 H2). destruct H3. assert (hd_rules_graph S D x0 x1). eapply hd_rules_graph_incl. apply H. hyp. unfold hd_rules_graph in H3. intuition. clear H7. ded (approx_correct H4). unfold Graph in H6. unfold co_scc in H0. rewrite forallb_forall in H0. ded (H0 _ H5). clear H0. rewrite forallb_forall in H7. ded (H7 _ H3). rewrite H6 in H0. discr. Qed.
imports: CoLoR(AGraph Union ATrs RelUtil ListUtil LogicUtil SN BoolUtil VecUtil)