Hi there,

I have a theorem stating that if a binary relation can be split as the union of two other relations (R = union R1 R2) than a certain property holds, where the union is defined inductively:

Definition Rel (A:Type) := A → A → Prop.

Inductive union {A} (red1 red2: Rel A) : Rel A :=

| union_left: forall a b, red1 a b → union red1 red2 a b

| union_right: forall a b, red2 a b → union red1 red2 a b.

Theorem mytheorem {A:Type}: forall (R :Rel A), exists (R1 R2: Rel A), R = (union R1 R2) /\ …

In other project, I defined the relation lx inductively as follows:

Inductive lx: Rel pterm :=

| b_ctx_rule : forall t u, b_ctx t u → lx t u

| x_ctx_rule : forall t u, x_ctx t u → lx t u.

Now I need to prove that lx = union b_ctx x_ctx in order to use my theorem:

1 subgoal (ID 333)

============================

lx = union b_ctx x_ctx

Is it possible to do so? In other words, is an inductive defined relation “equal” to the union of its constructors?

Any comment suggestion is very much appreciated.