Deductions# Deductions Top-level deductions Targets Expansions Locations and libpaths Nodes Labels and languages TeX labels Doc labels Other syntaxes Cf references Node Types Assertion nodes Intro nodes Supposition nodes Existential nodes Method nodes Citation nodes Falsum nodes Relation chain nodes Subdeductions Contradictions and Cases Proof by contradiction Proof by cases Using auxiliary deducs WOLOG WOLOG without reduction method WOLOG with reduction method Downward Flow