proposition: Lemma pweqeq_mon {R1 R2} (RR1 RR2 : R1 -> R2 -> Prop) X1 X2 (p : X1 = X2) k1 k2 : (forall r1 r2, RR1 r1 r2 -> RR2 r1 r2) -> pweqeq RR1 p k1 k2 -> pweqeq RR2 p k1 k2.
proof: Proof. destruct p; cbn; auto. Qed.
imports: Coq(Morphisms) ITree(Core.ITreeDefinition)