-(*
- Definition TInt : HaskType nil ★.
- assert (tyConKind' intPrimTyCon = ★).
- rewrite <- H.
- unfold HaskType; intros.
- apply TCon.
- Defined.
-
- Definition idproof1 : ND Rule [] [nil > nil > [TInt @@ nil] |- [TInt @@ nil]].
- apply nd_rule.
- apply RVar.
- Defined.