Interesting, I will probably try it out.

## Context:

Anyway, I will give a bit more context, since I can be potentially suffering from XY problem and solving an incorrect problem.

This question is connected to my previous question. Where I define an inductive `type`

representing types and a type `expr : type -> Type`

representing computations/programs.

Expressions are equivalent under a certain reduction. In the previous question I have asked how to implement this reduction. The part in the reduction is to reduce `Pair[Proj1[p]][Proj2[q]]`

to just ` p : X×Y`

. Reduction implemented using Equations plugin:

```
Equations? reduce {E : type} (e : E) : E :=
...
reduce (Pair[Proj1[p]][Proj2[q]]) := _;
...
reduce e := e.
(* if p ≡ q then p else pair[proj1[p]][proj2[q]] *)
destruct (dec_expr p q) as [eq | neq].
- inversion eq.
rewrite H0.
apply q.
- apply (pair[proj1[p]][proj2[q]]).
Defined.
```

I define an equality on expression that have the same computational behavior i.e. are the same under reduction `expr_eq_red`

, give the same result for all inputs `expr_eq_ext`

and equal programs preserve this equality `expr_eq_mor`

. (The symmetry and transitivity is there to make my life easier, I had trouble proving it, but that is a topic for another question)

```
Reserved Notation "x == y" (at level 70).
Inductive ExprEq : forall (X : type), X -> X -> Prop :=
| expr_eq_refl : forall {X : type}, forall (x : X), x == x
| expr_eq_sym : forall {X : type}, forall {x y : X}, x == y -> y == x
| expr_eq_tran : forall {X : type}, forall {x y z : X}, x == y -> y == z -> x == z
| expr_eq_ext : forall {X Y : type}, forall {f g : X --> Y}, (forall (x : X), f[x] == g[x]) -> f == g
| expr_eq_mor : forall {X Y : type} {f g : X --> Y} {x y : X}, f == g -> x == y -> f[x] == g[y]
| expr_eq_red : forall {X : type} (x : X), (reduce x) == x
where
"x == y" := (ExprEq _ x y).
```

Under these definitions, I have trouble proving the following lemma:

```
Lemma pair_identity : forall {X Y : type} (p : X × Y), pair[proj1[p]][proj2[p]] == p.
Proof.
intros.
pose proof (expr_eq_red pair[proj1[p]][proj2[p]]) as p'.
(* what now?*)
admit.
Admitted.
```

`p'`

does not reduce to `p`

because `dec_expr p p`

cannot be reduced to `left eq_refl`

in the definition of `reduce`