<div dir="ltr"><div class="gmail_extra">Hello,</div><div class="gmail_extra"><br></div><div class="gmail_extra">I hope I am not misunderstanding your question but I believe the answer is that this step is never done</div><div class="gmail_extra">explicitly.</div><div class="gmail_extra"><br></div><div class="gmail_extra">The iris-coq formalization is a shallow embedding so there is no explicit Coq datatype for the syntax of base logic terms. </div><div class="gmail_extra">Functions are represented as normal Coq functions so there is no need to explicitly specify the typing rules governing</div><div class="gmail_extra">them: they're built into Coq. Similarly with products, sums, etc. Once the type of propositions, iProp, is defined in Coq</div><div class="gmail_extra">Iris propositions are just represented as  normal Coq terms belong to iProp.</div><div class="gmail_extra"><br></div><div class="gmail_extra">I think that there should then really be no analog of 5.2 explicitly, it's encompassed in how the object terms</div><div class="gmail_extra">are represented in Coq in the first place.</div><div class="gmail_extra"><br></div><div class="gmail_extra">This is why, for instance, the definition of weakest preconditions we are able to take a guarded fixed point of</div><div class="gmail_extra">a normal Coq function (see wp_def in theories/program_logic/<wbr>weakestpre.v).</div><div class="gmail_extra"><br></div><div class="gmail_extra">Danny</div></div>