fact: Definition local_rec_beta {X} `{IsLocal f X} {i} (g : lgen_domain f i -> X) s : local_rec g (f i s) = g s := (fst (ooextendable_islocal i 1%nat) g).2 s.
imports: HoTT.Basics HoTT.Types Extensions ReflectiveSubuniverse Accessible