take the StackAlgebra /== ; :: thesis: the StackAlgebra /== is proper-for-identity
thus the StackAlgebra /== is proper-for-identity ; :: thesis: verum