<div dir="ltr"><div>Hi there,</div><div><br></div><div>when following the kripke semantics file of the Iowa Agda Library:</div><div><a href="https://github.com/cedille/ial/blob/master/kripke-semantics.agda#L37" target="_blank">https://github.com/cedille/ial/blob/master/kripke-semantics.agda#L37</a></div><div><br></div><div>we find in L37:<br></div><div>sample-pf = ImpliesI{$ "p"} (AndI (Assume{[]}) (Assume))</div><div>which is a proof of type [] ⊢ Implies ($ "p") (And ($ "p") ($ "p"))</div><div><br></div><div>i tested<br></div><div>sample-pf-alt = ImpliesI (AndI (Assume{[]} {($ "p")}) (Assume{[]} {($ "p")}))</div><div>and results also in a proof of the same type</div><div><br></div><div>What kind of syntactic sugar is making agda understand sample-pf without explicitly telling Assume its parameters in the first place?<br></div><div><br></div><div>best, herminie<br></div></div>