Index
| /\ | 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 |
| SingFunction1 | Proof.Equational |
| SingFunction2 | Proof.Equational |
| SingFunction3 | Proof.Equational |
| SingFunction4 | Proof.Equational |
| SingFunction5 | Proof.Equational |
| SingFunction6 | Proof.Equational |
| SingFunction7 | 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 |
| TyFun | Proof.Equational |
| unSingFun1 | Proof.Equational |
| unSingFun2 | Proof.Equational |
| unSingFun3 | Proof.Equational |
| unSingFun4 | Proof.Equational |
| unSingFun5 | Proof.Equational |
| unSingFun6 | Proof.Equational |
| unSingFun7 | Proof.Equational |
| unWrap | Proof.Equational |
| withSing | Proof.Equational |
| withSingI | Proof.Equational |
| withSomeSing | Proof.Equational |
| wrap | Proof.Equational |
| \/ | Proof.Propositional |