First-Order Logic in Coq Contributing to the Coq Library for First-Order Logic Tree Borrows The Semantics, The Program Logic, And All The Rest
