Hi All, does anybody know what they're doing with this bracket notation here in Coq'Art? Theyre saying this series of judgements describes existentials.
They did say earlier that  lists type judgements, but even if so I'm not sure I understand what they're then saying here.
oopsadaisy, this is super easy, they're just giving the derivation tree for ex.
Jacob Salzberg has marked this topic as resolved.
Looks like the brackets are a typo. Sorry!
Last updated: Feb 01 2023 at 12:30 UTC