proposition: Lemma compat_app : forall R R', compat R -> compat R' -> compat (R ++ R').
proof: Proof. intros R R' Rsucc R'succ l r lr. destruct (in_app_or lr). apply Rsucc. hyp. apply R'succ. hyp. Qed.
imports: CoLoR(ATrs RelUtil ListUtil ARelation SN LogicUtil)