proposition: Lemma prod_add_incl_tc_id : forall x y g, prod (XSet.add x (preds x g)) (XSet.add y (succs y g)) << (g U id x y)!.
proof: Proof. intros x y g a b. unfold prod. rewrite !add_iff. rewrite In_preds_rel, In_succs_rel. split_all. apply t_step. firstorder auto with crelations. apply t_trans with x; apply t_step; firstorder auto with crelations. apply t_trans with y; apply t_step; firstorder auto with crelations. apply t_trans with x. firstorder auto with sets. apply t_trans with y; apply t_step; firstorder auto with crelations. Qed.
imports: Coq(OrderedType) CoLoR(ListUtil FSetUtil FMapUtil RelUtil LogicUtil)