let R i (x y: M C i) := x = construct (destruct y)
I : Type u₀
C : IContainer I
i : I
x : M C i
⊢ construct (destruct x) = x
I : Type u₀
C : IContainer I
i : I
x : M C i
R : (i : I) → M C i → M C i → Prop := fun i x y => x = construct (destruct y)
⊢ construct (destruct x) = x