--#include "Alfa/Types.alfa" --#include "Alfa/PropositionalCalculus.alfa" --#include "Alfa/PredicateCalculus.alfa" --#include "Alfa/Identity.alfa" package Logic where public open Propositions use Prop, Absurdity, AbsurdityElim, Triviality, TrivialityIntro, Pred, Rel, NDGoal, IsTrue public open Propositional use And, AndIntro, AndElim1, AndElim2, AndElimCont, Or, OrIntro1, OrIntro2, OrElim, Implies, ImpliesIntro, ImpliesElim, Not, NotElim, Equivalence public open PredicateCalculus use ForAll, ForAllI, ForAllElim, Exists, ExistsIntro, ExistsElim public open Identity use refl, subst, substSym, sym, trans, cong, cong2, cong1 (===) :: (A::Set) -> (a::A) -> (b::A) -> Set = Identity.(==) {-# Alfa unfoldgoals off brief on hidetypeannots off wide nd hiding on var "NDGoal" proofgoal var "Absurdity" as "^" with symbolfont var "AbsurditElim" hide 1 var "AbsurdityElim" hide 1 as "^E" with symbolfont var "Triviality" as "T" with symbolfont var "TrivialityIntro" as "TI" with symbolfont var "And" infix 3 as "Ù" with symbolfont var "AndIntro" hide 2 as "ÙI" with symbolfont var "AndElim1" hide 2 as "ÙE1" with symbolfont var "AndElim2" hide 2 as "ÙE2" with symbolfont var "Or" infix 2 as "Ú" with symbolfont var "OrIntro1" hide 2 as "ÚI1" with symbolfont var "OrIntro2" hide 2 as "ÚI2" with symbolfont var "OrElim" hide 3 as "ÚE" with symbolfont var "Implies" infix rightassoc 1 as "®" with symbolfont var "ImpliesIntro" hide 2 as "®I" with symbolfont var "ImpliesElim" hide 2 as "®E" with symbolfont var "Equivalence" infix 1 as "«" with symbolfont var "Not" as "Ø" with symbolfont con "AndI" infix 3 as "ÙI" with symbolfont var "AndElimCont" hide 3 as "ÙE+" with symbolfont var "NotElim" hide 1 as "ØE" with symbolfont var "ForAll" hide 1 quantifier domain on as "\"" with symbolfont var "ForAllI" hide 2 as "\"I" with symbolfont var "ForAllElim" hide 3 as "\"E" with symbolfont var "Exists" hide 1 quantifier domain on as "$" with symbolfont var "ExistsIntro" hide 2 as "$I" with symbolfont var "ExistsElim" hide 3 as "$E" with symbolfont con "existsI" as "$I" with symbolfont con "forallI" as "\"I" with symbolfont var "===" distfix3 4 var "refl" hide 2 var "subst" hide 3 var "substSym" hide 3 var "sym" hide 3 var "trans" hide 4 var "cong" hide 4 var "cong2" hide 7 var "cong1" hide 6 #-}