Coq

Standard Library | The Coq Proof Assistant

• url: https://coq.inria.fr/doc/V8.19.0/stdlib/ .

implication - Transitivity of -> in Coq - Stack Overflow

• url: https://stackoverflow.com/questions/55295029/transitivity-of-in-coq

.

proof - Proving (\~A -> \~B)-> (\~A -> B) -> A in Coq - Stack Overflow

• url: https://stackoverflow.com/questions/55232025/proving-a-b-a-b-a-in-coq

.

coq - Proving f (f bool) = bool - Stack Overflow

• url: https://stackoverflow.com/questions/1674018/proving-f-f-bool-bool

.

DProp.Prop

• url: https://dunnl.github.io/dprop/DProp.Prop.html

.

Address a \"setoid hell\"? · Issue #10871 · coq/coq

• url: https://github.com/coq/coq/issues/10871

.

coq - Defining Kripke models and the canonical model for $S4$ modal logic - Proof Assistants Stack Exchange

• url: https://proofassistants.stackexchange.com/questions/2312/defining-kripke-models-and-the-canonical-model-for-s4-modal-logic
• topics: Coq, Modal Logic

.