proposition: Lemma Frs_iso : forall R, unlab_rules (lab_rules R) [=] R.
proof: Proof. intros R [l r]. split. intros [[l' r'] [h1 h2]]. destruct h1 as [[x y] [v [h h']]]. inversion h'. inversion h2. subst. rewrite !Ft_epi. hyp. unfold Frs. intro. set (v := fun x : variable => some_elt I). exists (mkRule (lab v l) (lab v r)). split. unfold lab_rules. exists (mkRule l r). exists v. intuition. simpl. rewrite !Ft_epi. refl. Qed.
imports: CoLoR(ATrs AInterpretation BoolUtil LogicUtil EqUtil VecUtil SN RelUtil AWFMInterpretation NaryFunction NatUtil ARelation ARules SetUtil FunUtil VecMax AMorphism) Coq(List)