let R (x y: M C) := x = construct (destruct y)
C : Container
x : M C
⊢ construct (destruct x) = x
C : Container
x : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
⊢ construct (destruct x) = x