TYPE: Show that semantic entailment for Type * is equivalent to semantic entailment for Type

[teorth]

This is a technical request, inspired by a comment at #36. It could be useful to have some way within Lean to show that the assertions

``theorem (G: Type *) [Magma G] (h: EquationX G): EquationY G`

and

theorem (G: Type) [Magma G] (h: EquationX G): EquationY G`

are equivalent to each other (or to LawX implying LawY). Similarly for the counterexamples to such implications. This type reduction should be achievable through the completeness theorem.

[codyroux]

claim

[codyroux]

I am sadly defeated by the universe handling in Lean.

[codyroux]

disclaim