Basic

Statistics

Metric	Count
Definitions `Proof`, `ax'`, `bot_inversion`, `cut'`, `parr_inversion`, `rwConclusion`, `with_inversion₁`, `with_inversion₂`, `Proposition`, `Equiv`, `bang_top_eqv_one`, `chooseEquiv`, `dual`, `equiv`, `refl`, `symm`, `trans`, `linImpl`, `negative`, `negative_decidable`, `oplus_idem`, `parr_top_eqv_top`, `positive`, `positive_decidable`, `propositionSetoid`, `quest_zero_eqv_bot`, `subst_eqv`, `subst_eqv_head`, `tensor_assoc`, `tensor_distrib_oplus`, `tensor_symm`, `tensor_zero_eqv_zero`, `with_idem`, `Sequent`, `Provable`, `toProof`, `allQuest`, `instBEqProposition`, `beq`, `instBotProposition`, `instCoeEquivEquiv`, `instCoeProofProvable`, `instDecidableEqProposition`, `decEq`, `instOneProposition`, `instTopProposition`, `instZeroProposition`, `term!_`, `term_⅋_`, `«term_&_»`, `«term_≡_»`, `«term_≡⇓_»`, `«term_⊕_»`, `«term_⊗_»`, `«term_⊸_»`, `«term_⫠»`, `«termʔ_»`, `«term⇓_»`	58
Theorems `refl`, `symm`, `trans`, `add_middle_eq_cons`, `dual_inj`, `dual_involution`, `dual_neq`, `dual_sizeOf`, `toProp`, `instSymmProvableConsTensor`, `top_eq_zero_dual`, `fromProof`	12
Total	70

Name	Category	Theorems
`Proof` 📖	CompData	—
`Proposition` 📖	CompData	4 math, 1 bridge math: `Proposition.add_middle_eq_cons`, `Proposition.dual_sizeOf`, `Proposition.top_eq_zero_dual`, `Proposition.instSymmProvableConsTensor` bridge: `Proof.expand_onlyAtomicAxioms`
`Sequent` 📖	CompOp	1 bridge bridge: `Proof.expand_onlyAtomicAxioms`
`instBEqProposition` 📖	CompOp	—
`instBotProposition` 📖	CompOp	—
`instCoeEquivEquiv` 📖	CompOp	—
`instCoeProofProvable` 📖	CompOp	—
`instDecidableEqProposition` 📖	CompOp	—
`instOneProposition` 📖	CompOp	—
`instTopProposition` 📖	CompOp	1 math math: `Proposition.top_eq_zero_dual`
`instZeroProposition` 📖	CompOp	1 math math: `Proposition.top_eq_zero_dual`
`term!_` 📖	CompOp	—
`term_⅋_` 📖	CompOp	—
`«term_&_»` 📖	CompOp	—
`«term_≡_»` 📖	CompOp	—
`«term_≡⇓_»` 📖	CompOp	—
`«term_⊕_»` 📖	CompOp	—
`«term_⊗_»` 📖	CompOp	—
`«term_⊸_»` 📖	CompOp	—
`«term_⫠»` 📖	CompOp	—
`«termʔ_»` 📖	CompOp	—
`«term⇓_»` 📖	CompOp	—

Name	Category	Theorems
`ax'` 📖	CompOp	—
`bot_inversion` 📖	CompOp	—
`cut'` 📖	CompOp	—
`parr_inversion` 📖	CompOp	—
`rwConclusion` 📖	CompOp	1 bridge bridge: `onlyAtomicAxioms_rwConclusion`
`with_inversion₁` 📖	CompOp	—
`with_inversion₂` 📖	CompOp	—

Name	Category	Theorems
`Equiv` 📖	MathDef	2 math math: `Equiv.refl`, `equiv.toProp`
`bang_top_eqv_one` 📖	CompOp	—
`chooseEquiv` 📖	CompOp	—
`dual` 📖	CompOp	4 math, 1 bridge math: `dual_involution`, `dual_inj`, `dual_sizeOf`, `top_eq_zero_dual` bridge: `Cslib.CLL.Proof.expand_onlyAtomicAxioms`
`equiv` 📖	CompOp	—
`linImpl` 📖	CompOp	—
`negative` 📖	CompOp	—
`negative_decidable` 📖	CompOp	—
`oplus_idem` 📖	CompOp	—
`parr_top_eqv_top` 📖	CompOp	—
`positive` 📖	CompOp	—
`positive_decidable` 📖	CompOp	—
`propositionSetoid` 📖	CompOp	—
`quest_zero_eqv_bot` 📖	CompOp	—
`subst_eqv` 📖	CompOp	—
`subst_eqv_head` 📖	CompOp	—
`tensor_assoc` 📖	CompOp	—
`tensor_distrib_oplus` 📖	CompOp	—
`tensor_symm` 📖	CompOp	—
`tensor_zero_eqv_zero` 📖	CompOp	—
`with_idem` 📖	CompOp	—

Name	Kind	Assumes	Proves	Validates	Depends On
`add_middle_eq_cons` 📖	mathematical	—	`Cslib.CLL.Proposition`	—	—
`dual_inj` 📖	mathematical	—	`dual`	—	—
`dual_involution` 📖	mathematical	—	`dual`	—	—
`dual_neq` 📖	—	—	—	—	—
`dual_sizeOf` 📖	mathematical	—	`Cslib.CLL.Proposition` `dual`	—	—
`instSymmProvableConsTensor` 📖	mathematical	—	`Cslib.CLL.Proposition` `Cslib.CLL.Sequent.Provable` `tensor`	—	`Cslib.CLL.Sequent.Provable.fromProof`
`top_eq_zero_dual` 📖	mathematical	—	`Cslib.CLL.Proposition` `Cslib.CLL.instTopProposition` `dual` `Cslib.CLL.instZeroProposition`	—	—

Name	Kind	Assumes	Proves	Validates	Depends On
`refl` 📖	mathematical	—	`Cslib.CLL.Proposition.Equiv`	—	`Cslib.CLL.Proposition.equiv.toProp`
`symm` 📖	—	`Cslib.CLL.Proposition.Equiv`	—	—	—
`trans` 📖	—	`Cslib.CLL.Proposition.Equiv`	—	—	`Cslib.CLL.Sequent.Provable.fromProof`

Name	Kind	Assumes	Proves	Validates	Depends On
`toProp` 📖	mathematical	—	`Cslib.CLL.Proposition.Equiv`	—	`Cslib.CLL.Sequent.Provable.fromProof`

Name	Category	Theorems
`Provable` 📖	MathDef	2 math math: `Provable.fromProof`, `Cslib.CLL.Proposition.instSymmProvableConsTensor`
`allQuest` 📖	CompOp	—

Name	Category	Theorems
`toProof` 📖	CompOp	—

Name	Kind	Assumes	Proves	Validates	Depends On
`fromProof` 📖	mathematical	—	`Cslib.CLL.Sequent.Provable`	—	—

Name	Category	Theorems
`beq` 📖	CompOp	—

Name	Category	Theorems
`decEq` 📖	CompOp	—

---