/\ | Proof.Propositional |
:/\: | Proof.Equational |
:=: | Proof.Equational |
:\/: | Proof.Equational |
:~: | Proof.Equational |
:~> | Proof.Equational |
=<= | Proof.Equational |
=== | Proof.Equational |
=>= | Proof.Equational |
=~= | Proof.Equational |
@@ | Proof.Equational |
admitted | Proof.Equational |
andAssocL | Proof.Propositional |
andAssocR | Proof.Propositional |
andElimL | Proof.Propositional |
andElimR | Proof.Propositional |
andIntro | Proof.Propositional |
Apply | Proof.Equational |
apply | Proof.Equational |
applySing | Proof.Equational |
Args | Proof.Equational |
asProxyTypeOf | Proof.Equational |
Because | Proof.Equational |
because | Proof.Equational |
bugInGHC | Proof.Equational |
by | Proof.Equational |
byDefinition | Proof.Equational |
coerce | Proof.Equational |
coerce' | Proof.Equational |
cong | Proof.Equational |
cong' | Proof.Equational |
Demote | Proof.Equational |
DemoteRep | Proof.Equational |
Equality | Proof.Equational |
exfalso | Proof.Propositional |
FromBool | Proof.Equational |
fromBool | Proof.Equational |
fromLeibniz | Proof.Equational |
fromRefl | Proof.Equational |
fromSing | Proof.Equational |
genInduction | Proof.Induction |
KindOf | Proof.Equational |
KProxy | |
1 (Data Constructor) | Proof.Equational |
2 (Type/Class) | Proof.Equational |
Leibniz | |
1 (Type/Class) | Proof.Equational |
2 (Data Constructor) | Proof.Equational |
leibnizToRefl | Proof.Equational |
Not | Proof.Propositional |
orAssocL | Proof.Propositional |
orAssocR | Proof.Propositional |
orElim | Proof.Propositional |
OriginalProp | Proof.Equational |
orIntroL | Proof.Propositional |
orIntroR | Proof.Propositional |
Predicate | Proof.Equational |
Preorder | Proof.Equational |
Proposition | Proof.Equational |
Proxy | |
1 (Data Constructor) | Proof.Equational |
2 (Type/Class) | Proof.Equational |
Reason | Proof.Equational |
Refl | Proof.Equational |
reflexivity | Proof.Equational |
reflexivity' | Proof.Equational |
reflToLeibniz | Proof.Equational |
Sing | Proof.Equational |
sing | Proof.Equational |
singByProxy | Proof.Equational |
singByProxy# | Proof.Equational |
singFun1 | Proof.Equational |
singFun2 | Proof.Equational |
singFun3 | Proof.Equational |
singFun4 | Proof.Equational |
singFun5 | Proof.Equational |
singFun6 | Proof.Equational |
singFun7 | Proof.Equational |
singFun8 | Proof.Equational |
SingFunction1 | Proof.Equational |
SingFunction2 | Proof.Equational |
SingFunction3 | Proof.Equational |
SingFunction4 | Proof.Equational |
SingFunction5 | Proof.Equational |
SingFunction6 | Proof.Equational |
SingFunction7 | Proof.Equational |
SingFunction8 | Proof.Equational |
SingI | Proof.Equational |
SingInstance | |
1 (Data Constructor) | Proof.Equational |
2 (Type/Class) | Proof.Equational |
singInstance | Proof.Equational |
SingKind | Proof.Equational |
singThat | Proof.Equational |
SLambda | Proof.Equational |
SomeSing | |
1 (Data Constructor) | Proof.Equational |
2 (Type/Class) | Proof.Equational |
start | Proof.Equational |
sym | Proof.Equational |
symmetry | Proof.Equational |
toSing | Proof.Equational |
trans | Proof.Equational |
transitivity | Proof.Equational |
TyCon1 | Proof.Equational |
TyCon2 | Proof.Equational |
TyCon3 | Proof.Equational |
TyCon4 | Proof.Equational |
TyCon5 | Proof.Equational |
TyCon6 | Proof.Equational |
TyCon7 | Proof.Equational |
TyCon8 | Proof.Equational |
TyFun | Proof.Equational |
unSingFun1 | Proof.Equational |
unSingFun2 | Proof.Equational |
unSingFun3 | Proof.Equational |
unSingFun4 | Proof.Equational |
unSingFun5 | Proof.Equational |
unSingFun6 | Proof.Equational |
unSingFun7 | Proof.Equational |
unSingFun8 | Proof.Equational |
unWrap | Proof.Equational |
withSing | Proof.Equational |
withSingI | Proof.Equational |
withSomeSing | Proof.Equational |
wrap | Proof.Equational |
\/ | Proof.Propositional |