The Coq mailing list

[Gregory Bush <gbush AT mysck.com>]

(* This may be trivial, but is the following provable in Coq without  
using JMeq_eq or other axioms? *)


Set Implicit Arguments.

Variable M : Type -> Type.

Variable R : forall A, M A -> M A -> Prop.

Inductive R' : forall A B, M A -> M B -> Prop :=
| CR' : forall A (x y : M A), R x y -> R' x y.

Theorem R'inv : forall A (x y : M A), R' x y -> R x y.


(* Thanks *)