D.pure_program_logic.weakestpre

D.pure_program_logic.lifting

D.pure_program_logic.adequacy

D.iris_extra.det_reduction

D.iris_extra.cmra_prop_lift

D.iris_extra.dlang

D.iris_extra.iris_prelude

D.iris_extra.lty

D.iris_extra.persistence

D.iris_extra.proofmode_extra

D.iris_extra.saved_interp_dep

D.iris_extra.swap_later_impl

D.prelude

D.asubst_intf

D.asubst_base

D.proper

D.succ_notation

D.tactics

D.Dot.syn.syn

D.Dot.syn.rules

D.Dot.syn.path_repl

D.Dot.syn.path_repl_lemmas

D.Dot.syn.lr_syn_aux

D.Dot.syn.drop_skips

D.Dot.syn.skeleton

D.Dot.syn.core_stamping_defs

D.Dot.syn.traversals

D.Dot.lr.dlang_inst

D.Dot.lr.dot_lty

D.Dot.lr.later_sub_sem

D.Dot.lr.path_wp

D.Dot.lr.unary_lr

D.Dot.lr.sem_unstamped_typing

D.Dot.semtyp_lemmas.binding_lr

D.Dot.semtyp_lemmas.defs_lr

D.Dot.semtyp_lemmas.dsub_lr

D.Dot.semtyp_lemmas.path_repl_lr

D.Dot.semtyp_lemmas.prims_lr

D.Dot.semtyp_lemmas.tproj_lr

D.Dot.typing.subtyping

D.Dot.typing.type_eq

D.Dot.typing.typing

D.Dot.typing.typing_aux_defs

D.Dot.fundamental

D.Dot.examples.ex_utils

D.Dot.examples.hoas

D.Dot.examples.hoas_ex_utils

D.Dot.examples.stamping.unstampedness_binding

D.Dot.examples.old_typing.old_subtyping

D.Dot.examples.old_typing.old_subtyping_derived_rules

D.Dot.examples.old_typing.old_unstamped_typing

D.Dot.examples.old_typing.old_unstamped_typing_derived_rules

D.Dot.examples.old_typing.old_unstamped_typing_to_typing

D.Dot.examples.old_fundamental

D.Dot.examples.sem.semtyp_lemmas.sub_lr

D.Dot.examples.sem.semtyp_lemmas.examples_lr

D.Dot.examples.sem.ex_iris_utils

D.Dot.examples.sem.no_russell_paradox

D.Dot.examples.sem.prim_boolean_option

D.Dot.examples.sem.storeless_typing

D.Dot.examples.sem.storeless_typing_ex

D.Dot.examples.sem.storeless_typing_ex_utils

D.Dot.examples.sem.from_pdot_mutual_rec_sem

D.Dot.examples.sem.small_sem_ex

D.Dot.examples.sem.positive_div

D.Dot.examples.syn.from_pdot_mutual_rec

D.Dot.examples.syn.list

D.Dot.examples.syn.old_unstamped_typing_ex

D.Dot.examples.syn.scala_lib

D.Dot.examples.syn.syn_lemmas

D.Dot.hkdot.sem_kind

D.Dot.hkdot.hkdot

D.DSub.syn.ds_rules

D.DSub.syn.ds_syn

D.DSub.syn.ds_syn_lemmas

D.DSub.lr.ds_ty_interp_subst_lemmas

D.DSub.lr.ds_unary_lr

D.DSub.lr.ds_semtyp_lemmas

D.DSub.typing.ds_obj_ident_typing

D.DSub.typing.ds_storeless_typing

D.DSub.ds_fundamental