proposition: Lemma R__P_I__P p: R__P (I__P p) = p.
proof: Proof. unfold I__P; destruct p as [m n]; induction (diagId m n); cbn. - reflexivity. - now rewrite IHd. - now rewrite IHd. Qed.
imports: FinFun Undecidability.HOU(std.decidable)