| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1106 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (178 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (320 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (18 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (389 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (25 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (81 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (27 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (68 entries) |
Global Index
D
DecidableTypeWithLeibniz [module, in DeBrLevel.Core.LevelInterface]DecidableTypeWithLeibniz.eq_leibniz [axiom, in DeBrLevel.Core.LevelInterface]
E
EqualityTypeWithLeibniz [module, in DeBrLevel.Core.LevelInterface]EqualityTypeWithLeibniz.eq_leibniz [axiom, in DeBrLevel.Core.LevelInterface]
H
HasShift [module, in DeBrLevel.Core.LevelInterface]HasShift.shift [axiom, in DeBrLevel.Core.LevelInterface]
HasShift.shift_eq [instance, in DeBrLevel.Core.LevelInterface]
HasShift.specs [section, in DeBrLevel.Core.LevelInterface]
HasShift.specs.k [variable, in DeBrLevel.Core.LevelInterface]
HasShift.specs.m [variable, in DeBrLevel.Core.LevelInterface]
HasShift.specs.n [variable, in DeBrLevel.Core.LevelInterface]
HasShift.specs.p [variable, in DeBrLevel.Core.LevelInterface]
HasShift.specs.shift_eq_iff [variable, in DeBrLevel.Core.LevelInterface]
HasShift.specs.shift_unfold_1 [variable, in DeBrLevel.Core.LevelInterface]
HasShift.specs.shift_unfold [variable, in DeBrLevel.Core.LevelInterface]
HasShift.specs.shift_permute [variable, in DeBrLevel.Core.LevelInterface]
HasShift.specs.shift_trans [variable, in DeBrLevel.Core.LevelInterface]
HasShift.specs.shift_zero_refl [variable, in DeBrLevel.Core.LevelInterface]
HasShift.specs.t [variable, in DeBrLevel.Core.LevelInterface]
HasShift.specs.t' [variable, in DeBrLevel.Core.LevelInterface]
I
IsBdlLvl [module, in DeBrLevel.Core.LevelInterface]IsBdlLvlDT [module, in DeBrLevel.Core.LevelInterface]
IsBdlLvlDTWL [module, in DeBrLevel.Core.LevelInterface]
IsBdlLvlET [module, in DeBrLevel.Core.LevelInterface]
IsBdlLvlETWL [module, in DeBrLevel.Core.LevelInterface]
IsBdlLvlFullDT [module, in DeBrLevel.Core.LevelInterface]
IsBdlLvlFullDTWL [module, in DeBrLevel.Core.LevelInterface]
IsBdlLvlFullET [module, in DeBrLevel.Core.LevelInterface]
IsBdlLvlFullETWL [module, in DeBrLevel.Core.LevelInterface]
IsBdlLvlFullListETWL [module, in DeBrLevel.Datatype.ListLevel]
IsBdlLvlFullListETWL.shift_wf_refl [lemma, in DeBrLevel.Datatype.ListLevel]
IsBdlLvlFullMapDInterface [module, in DeBrLevel.Map.MapLevelInterface]
IsBdlLvlFullMapKDInterface [module, in DeBrLevel.Map.MapLevelInterface]
IsBdlLvlFullMapKInterface [module, in DeBrLevel.Map.MapLevelInterface]
IsBdlLvlFullMapLVLDInterface [module, in DeBrLevel.Map.MapLevelInterface]
IsBdlLvlFullMapLVLInterface [module, in DeBrLevel.Map.MapLevelInterface]
IsBdlLvlFullOptET [module, in DeBrLevel.Datatype.OptionLevel]
IsBdlLvlFullOptETWL [module, in DeBrLevel.Datatype.OptionLevel]
IsBdlLvlFullOptETWL.eq_leibniz [lemma, in DeBrLevel.Datatype.OptionLevel]
IsBdlLvlFullOptET.shift_wf_refl [lemma, in DeBrLevel.Datatype.OptionLevel]
IsBdlLvlFullOT [module, in DeBrLevel.Core.LevelInterface]
IsBdlLvlFullOTWL [module, in DeBrLevel.Core.LevelInterface]
IsBdlLvlFullPairET [module, in DeBrLevel.Datatype.PairLevel]
IsBdlLvlFullPairETWL [module, in DeBrLevel.Datatype.PairLevel]
IsBdlLvlFullPairETWL.eq_leibniz [lemma, in DeBrLevel.Datatype.PairLevel]
IsBdlLvlFullPairET.shift_wf_refl [lemma, in DeBrLevel.Datatype.PairLevel]
IsBdlLvlFullPairOT [module, in DeBrLevel.Datatype.PairLevel]
IsBdlLvlFullPairOTWL [module, in DeBrLevel.Datatype.PairLevel]
IsBdlLvlFullPairOTWL.eq_leibniz [lemma, in DeBrLevel.Datatype.PairLevel]
IsBdlLvlFullPairOT.shift_wf_refl [lemma, in DeBrLevel.Datatype.PairLevel]
IsBdlLvlFullSet [module, in DeBrLevel.Set.SetLevel]
IsBdlLvlFullSetInterface [module, in DeBrLevel.Set.SetLevelInterface]
IsBdlLvlFullSet.shift_wf_refl [lemma, in DeBrLevel.Set.SetLevel]
IsBdlLvlFullSet.Wf_in_iff [lemma, in DeBrLevel.Set.SetLevel]
IsBdlLvlListETWL [module, in DeBrLevel.Datatype.ListLevel]
IsBdlLvlListETWL.shift_wf_refl [lemma, in DeBrLevel.Datatype.ListLevel]
IsBdlLvlMapD [module, in DeBrLevel.Map.MapLevelD]
IsBdlLvlMapDInterface [module, in DeBrLevel.Map.MapLevelInterface]
IsBdlLvlMapD.shift_wf_refl [lemma, in DeBrLevel.Map.MapLevelD]
IsBdlLvlMapK [module, in DeBrLevel.Map.MapLevelK]
IsBdlLvlMapKD [module, in DeBrLevel.Map.MapLevelKD]
IsBdlLvlMapKDInterface [module, in DeBrLevel.Map.MapLevelInterface]
IsBdlLvlMapKDInterface.shift_wf_refl [axiom, in DeBrLevel.Map.MapLevelInterface]
IsBdlLvlMapKDInterface.shift_find_Wf [axiom, in DeBrLevel.Map.MapLevelInterface]
IsBdlLvlMapKDInterface.Wf_in_iff [axiom, in DeBrLevel.Map.MapLevelInterface]
IsBdlLvlMapKD.shift_find_Wf [lemma, in DeBrLevel.Map.MapLevelKD]
IsBdlLvlMapKD.shift_wf_refl [lemma, in DeBrLevel.Map.MapLevelKD]
IsBdlLvlMapKD.Wf_in_iff [lemma, in DeBrLevel.Map.MapLevelKD]
IsBdlLvlMapKInterface [module, in DeBrLevel.Map.MapLevelInterface]
IsBdlLvlMapKInterface.shift_wf_refl [axiom, in DeBrLevel.Map.MapLevelInterface]
IsBdlLvlMapKInterface.shift_find_Wf [axiom, in DeBrLevel.Map.MapLevelInterface]
IsBdlLvlMapKInterface.Wf_in_iff [axiom, in DeBrLevel.Map.MapLevelInterface]
IsBdlLvlMapK.shift_find_Wf [lemma, in DeBrLevel.Map.MapLevelK]
IsBdlLvlMapK.shift_wf_refl [lemma, in DeBrLevel.Map.MapLevelK]
IsBdlLvlMapK.Wf_in_iff [lemma, in DeBrLevel.Map.MapLevelK]
IsBdlLvlMapLVL [module, in DeBrLevel.Map.MapLevelLvl]
IsBdlLvlMapLVLD [module, in DeBrLevel.Map.MapLevelLVLD]
IsBdlLvlMapLVLDInterface [module, in DeBrLevel.Map.MapLevelInterface]
IsBdlLvlMapLVLD.shift_wf_refl [lemma, in DeBrLevel.Map.MapLevelLVLD]
IsBdlLvlMapLVLInterface [module, in DeBrLevel.Map.MapLevelInterface]
IsBdlLvlMapLVL.shift_wf_refl [lemma, in DeBrLevel.Map.MapLevelLvl]
IsBdlLvlOptET [module, in DeBrLevel.Datatype.OptionLevel]
IsBdlLvlOptETWL [module, in DeBrLevel.Datatype.OptionLevel]
IsBdlLvlOptETWL.eq_leibniz [lemma, in DeBrLevel.Datatype.OptionLevel]
IsBdlLvlOptET.shift_wf_refl [lemma, in DeBrLevel.Datatype.OptionLevel]
IsBdlLvlOT [module, in DeBrLevel.Core.LevelInterface]
IsBdlLvlOTWL [module, in DeBrLevel.Core.LevelInterface]
IsBdlLvlPairET [module, in DeBrLevel.Datatype.PairLevel]
IsBdlLvlPairETWL [module, in DeBrLevel.Datatype.PairLevel]
IsBdlLvlPairETWL.eq_leibniz [lemma, in DeBrLevel.Datatype.PairLevel]
IsBdlLvlPairET.shift_wf_refl [lemma, in DeBrLevel.Datatype.PairLevel]
IsBdlLvlPairOT [module, in DeBrLevel.Datatype.PairLevel]
IsBdlLvlPairOTWL [module, in DeBrLevel.Datatype.PairLevel]
IsBdlLvlPairOTWL.eq_leibniz [lemma, in DeBrLevel.Datatype.PairLevel]
IsBdlLvlPairOT.shift_wf_refl [lemma, in DeBrLevel.Datatype.PairLevel]
IsBdlLvlSet [module, in DeBrLevel.Set.SetLevel]
IsBdlLvlSetInterface [module, in DeBrLevel.Set.SetLevelInterface]
IsBdlLvlSetInterface.shift_wf_refl [axiom, in DeBrLevel.Set.SetLevelInterface]
IsBdlLvlSetInterface.Wf_in_iff [axiom, in DeBrLevel.Set.SetLevelInterface]
IsBdlLvlSet.shift_wf_refl [lemma, in DeBrLevel.Set.SetLevel]
IsBdlLvlSet.Wf_in_iff [lemma, in DeBrLevel.Set.SetLevel]
IsBindlessLeveled [module, in DeBrLevel.Core.LevelInterface]
IsBindlessLeveledDT [module, in DeBrLevel.Core.LevelInterface]
IsBindlessLeveledDTWithLeibniz [module, in DeBrLevel.Core.LevelInterface]
IsBindlessLeveledET [module, in DeBrLevel.Core.LevelInterface]
IsBindlessLeveledETWithLeibniz [module, in DeBrLevel.Core.LevelInterface]
IsBindlessLeveledEx [module, in DeBrLevel.Core.LevelInterface]
IsBindlessLeveledEx.shift_wf_refl [axiom, in DeBrLevel.Core.LevelInterface]
IsBindlessLeveledFullDT [module, in DeBrLevel.Core.LevelInterface]
IsBindlessLeveledFullDTWithLeibniz [module, in DeBrLevel.Core.LevelInterface]
IsBindlessLeveledFullET [module, in DeBrLevel.Core.LevelInterface]
IsBindlessLeveledFullETWithLeibniz [module, in DeBrLevel.Core.LevelInterface]
IsBindlessLeveledFullOT [module, in DeBrLevel.Core.LevelInterface]
IsBindlessLeveledFullOTWithLeibniz [module, in DeBrLevel.Core.LevelInterface]
IsBindlessLeveledOT [module, in DeBrLevel.Core.LevelInterface]
IsBindlessLeveledOTWithLeibniz [module, in DeBrLevel.Core.LevelInterface]
IsBindlessLeveled.shift_wf_refl [axiom, in DeBrLevel.Core.LevelInterface]
IsLeveled [module, in DeBrLevel.Core.LevelInterface]
IsLeveledDT [module, in DeBrLevel.Core.LevelInterface]
IsLeveledDTWithLeibniz [module, in DeBrLevel.Core.LevelInterface]
IsLeveledET [module, in DeBrLevel.Core.LevelInterface]
IsLeveledETWithLeibniz [module, in DeBrLevel.Core.LevelInterface]
IsLeveledFullDT [module, in DeBrLevel.Core.LevelInterface]
IsLeveledFullDTWithLeibniz [module, in DeBrLevel.Core.LevelInterface]
IsLeveledFullET [module, in DeBrLevel.Core.LevelInterface]
IsLeveledFullETWithLeibniz [module, in DeBrLevel.Core.LevelInterface]
IsLeveledFullOT [module, in DeBrLevel.Core.LevelInterface]
IsLeveledFullOTWithLeibniz [module, in DeBrLevel.Core.LevelInterface]
IsLeveledOT [module, in DeBrLevel.Core.LevelInterface]
IsLeveledOTWithLeibniz [module, in DeBrLevel.Core.LevelInterface]
IsLeveled.specs [section, in DeBrLevel.Core.LevelInterface]
IsLeveled.specs.k [variable, in DeBrLevel.Core.LevelInterface]
IsLeveled.specs.m [variable, in DeBrLevel.Core.LevelInterface]
IsLeveled.specs.n [variable, in DeBrLevel.Core.LevelInterface]
IsLeveled.specs.p [variable, in DeBrLevel.Core.LevelInterface]
IsLeveled.specs.shift_preserves_wf_zero [variable, in DeBrLevel.Core.LevelInterface]
IsLeveled.specs.shift_preserves_wf_2 [variable, in DeBrLevel.Core.LevelInterface]
IsLeveled.specs.shift_preserves_wf_1 [variable, in DeBrLevel.Core.LevelInterface]
IsLeveled.specs.shift_preserves_wf [variable, in DeBrLevel.Core.LevelInterface]
IsLeveled.specs.shift_preserves_wf_gen [variable, in DeBrLevel.Core.LevelInterface]
IsLeveled.specs.t [variable, in DeBrLevel.Core.LevelInterface]
IsLvl [module, in DeBrLevel.Core.LevelInterface]
IsLvlDT [module, in DeBrLevel.Core.LevelInterface]
IsLvlDTWL [module, in DeBrLevel.Core.LevelInterface]
IsLvlET [module, in DeBrLevel.Core.LevelInterface]
IsLvlETWL [module, in DeBrLevel.Core.LevelInterface]
IsLvlFullDT [module, in DeBrLevel.Core.LevelInterface]
IsLvlFullDTWL [module, in DeBrLevel.Core.LevelInterface]
IsLvlFullET [module, in DeBrLevel.Core.LevelInterface]
IsLvlFullETWL [module, in DeBrLevel.Core.LevelInterface]
IsLvlFullListETWL [module, in DeBrLevel.Datatype.ListLevel]
IsLvlFullListETWL.is_wf_eq [lemma, in DeBrLevel.Datatype.ListLevel]
IsLvlFullListETWL.is_wf [definition, in DeBrLevel.Datatype.ListLevel]
IsLvlFullListETWL.notWf_is_wf_false [lemma, in DeBrLevel.Datatype.ListLevel]
IsLvlFullListETWL.props [section, in DeBrLevel.Datatype.ListLevel]
IsLvlFullListETWL.props.k [variable, in DeBrLevel.Datatype.ListLevel]
IsLvlFullListETWL.props.t [variable, in DeBrLevel.Datatype.ListLevel]
IsLvlFullListETWL.Wf_is_wf_true [lemma, in DeBrLevel.Datatype.ListLevel]
IsLvlFullMapDInterface [module, in DeBrLevel.Map.MapLevelInterface]
IsLvlFullMapKDInterface [module, in DeBrLevel.Map.MapLevelInterface]
IsLvlFullMapKInterface [module, in DeBrLevel.Map.MapLevelInterface]
IsLvlFullMapLVLDInterface [module, in DeBrLevel.Map.MapLevelInterface]
IsLvlFullMapLVLInterface [module, in DeBrLevel.Map.MapLevelInterface]
IsLvlFullOptET [module, in DeBrLevel.Datatype.OptionLevel]
IsLvlFullOptETWL [module, in DeBrLevel.Datatype.OptionLevel]
IsLvlFullOptETWL.eq_leibniz [lemma, in DeBrLevel.Datatype.OptionLevel]
IsLvlFullOptET.definition [section, in DeBrLevel.Datatype.OptionLevel]
IsLvlFullOptET.is_wf_eq [instance, in DeBrLevel.Datatype.OptionLevel]
IsLvlFullOptET.is_wf [definition, in DeBrLevel.Datatype.OptionLevel]
IsLvlFullOptET.notWf_is_wf_false [lemma, in DeBrLevel.Datatype.OptionLevel]
IsLvlFullOptET.valid [section, in DeBrLevel.Datatype.OptionLevel]
IsLvlFullOptET.valid.n [variable, in DeBrLevel.Datatype.OptionLevel]
IsLvlFullOptET.valid.t [variable, in DeBrLevel.Datatype.OptionLevel]
IsLvlFullOptET.Wf_is_wf_true [lemma, in DeBrLevel.Datatype.OptionLevel]
IsLvlFullOT [module, in DeBrLevel.Core.LevelInterface]
IsLvlFullOTWL [module, in DeBrLevel.Core.LevelInterface]
IsLvlFullPairET [module, in DeBrLevel.Datatype.PairLevel]
IsLvlFullPairETWL [module, in DeBrLevel.Datatype.PairLevel]
IsLvlFullPairETWL.eq_leibniz [lemma, in DeBrLevel.Datatype.PairLevel]
IsLvlFullPairET.is_wf_eq [instance, in DeBrLevel.Datatype.PairLevel]
IsLvlFullPairET.is_wf.t [variable, in DeBrLevel.Datatype.PairLevel]
IsLvlFullPairET.is_wf.n [variable, in DeBrLevel.Datatype.PairLevel]
IsLvlFullPairET.is_wf [section, in DeBrLevel.Datatype.PairLevel]
IsLvlFullPairET.is_wf [definition, in DeBrLevel.Datatype.PairLevel]
IsLvlFullPairET.notWf_is_wf_false [lemma, in DeBrLevel.Datatype.PairLevel]
IsLvlFullPairET.Wf_is_wf_true [lemma, in DeBrLevel.Datatype.PairLevel]
IsLvlFullPairOT [module, in DeBrLevel.Datatype.PairLevel]
IsLvlFullPairOTWL [module, in DeBrLevel.Datatype.PairLevel]
IsLvlFullPairOTWL.eq_leibniz [lemma, in DeBrLevel.Datatype.PairLevel]
IsLvlFullPairOT.is_wf_eq [lemma, in DeBrLevel.Datatype.PairLevel]
IsLvlFullPairOT.is_wf.t [variable, in DeBrLevel.Datatype.PairLevel]
IsLvlFullPairOT.is_wf.n [variable, in DeBrLevel.Datatype.PairLevel]
IsLvlFullPairOT.is_wf [section, in DeBrLevel.Datatype.PairLevel]
IsLvlFullPairOT.is_wf [definition, in DeBrLevel.Datatype.PairLevel]
IsLvlFullPairOT.notWf_is_wf_false [lemma, in DeBrLevel.Datatype.PairLevel]
IsLvlFullPairOT.Wf_is_wf_true [lemma, in DeBrLevel.Datatype.PairLevel]
IsLvlFullSet [module, in DeBrLevel.Set.SetLevel]
IsLvlFullSetInterface [module, in DeBrLevel.Set.SetLevelInterface]
IsLvlFullSet.is_wf_eq [instance, in DeBrLevel.Set.SetLevel]
IsLvlFullSet.is_wf [definition, in DeBrLevel.Set.SetLevel]
IsLvlFullSet.notWf_is_wf_false [lemma, in DeBrLevel.Set.SetLevel]
IsLvlFullSet.Wf_is_wf_true [lemma, in DeBrLevel.Set.SetLevel]
IsLvlListETWL [module, in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.eq [definition, in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.eq_leibniz [lemma, in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.eq_equiv [instance, in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.eq_trans [instance, in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.eq_sym [instance, in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.eq_refl [instance, in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.shift [definition, in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.shift_preserves_wf_zero [lemma, in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.shift_preserves_wf_2 [lemma, in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.shift_preserves_wf_gen [lemma, in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.shift_preserves_wf_1 [lemma, in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.shift_preserves_wf [lemma, in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.shift_notin [lemma, in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.shift_in_e [lemma, in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.shift_in [lemma, in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.shift_app [lemma, in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.shift_cons [lemma, in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.shift_nil [lemma, in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.shift_unfold_1 [lemma, in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.shift_unfold [lemma, in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.shift_permute [lemma, in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.shift_trans [lemma, in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.shift_zero_refl [lemma, in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.shift_eq_iff [lemma, in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.shift_eq [instance, in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.shift_props.t' [variable, in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.shift_props.t [variable, in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.shift_props.k'' [variable, in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.shift_props.k' [variable, in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.shift_props.k [variable, in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.shift_props.lb [variable, in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.shift_props [section, in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.t [definition, in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.Wf [definition, in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.Wf_weakening [lemma, in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.Wf_in [lemma, in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.Wf_app [lemma, in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.Wf_cons [lemma, in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.Wf_nil [lemma, in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.Wf_unfold [lemma, in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.Wf_iff [instance, in DeBrLevel.Datatype.ListLevel]
IsLvlMapD [module, in DeBrLevel.Map.MapLevelD]
IsLvlMapDInterface [module, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapDInterface.specs [section, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapDInterface.specs.k [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapDInterface.specs.m [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapDInterface.specs.m' [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapDInterface.specs.n [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapDInterface.specs.p [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapDInterface.specs.shift_find_iff [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapDInterface.specs.shift_notin_iff [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapDInterface.specs.shift_in_iff [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapDInterface.specs.shift_remove [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapDInterface.specs.shift_Add_iff [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapDInterface.specs.shift_Add [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapDInterface.specs.shift_add [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapDInterface.specs.shift_Empty [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapDInterface.specs.shift_Empty_iff [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapDInterface.specs.v [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapDInterface.specs.Wf_update [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapDInterface.specs.Wf_find [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapDInterface.specs.Wf_add [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapDInterface.specs.Wf_add_in [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapDInterface.specs.Wf_Add [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapDInterface.specs.Wf_Add_iff [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapDInterface.specs.Wf_empty [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapDInterface.specs.Wf_Empty [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapDInterface.specs.x [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapD.iff_equiv [instance, in DeBrLevel.Map.MapLevelD]
IsLvlMapD.logic_eq_equiv [instance, in DeBrLevel.Map.MapLevelD]
IsLvlMapD.shift [definition, in DeBrLevel.Map.MapLevelD]
IsLvlMapD.shift_preserves_wf_zero [lemma, in DeBrLevel.Map.MapLevelD]
IsLvlMapD.shift_preserves_wf [lemma, in DeBrLevel.Map.MapLevelD]
IsLvlMapD.shift_preserves_wf_2 [lemma, in DeBrLevel.Map.MapLevelD]
IsLvlMapD.shift_preserves_wf_gen [lemma, in DeBrLevel.Map.MapLevelD]
IsLvlMapD.shift_preserves_wf_1 [lemma, in DeBrLevel.Map.MapLevelD]
IsLvlMapD.shift_unfold_1 [lemma, in DeBrLevel.Map.MapLevelD]
IsLvlMapD.shift_unfold [lemma, in DeBrLevel.Map.MapLevelD]
IsLvlMapD.shift_permute [lemma, in DeBrLevel.Map.MapLevelD]
IsLvlMapD.shift_trans [lemma, in DeBrLevel.Map.MapLevelD]
IsLvlMapD.shift_zero_refl [lemma, in DeBrLevel.Map.MapLevelD]
IsLvlMapD.shift_remove [lemma, in DeBrLevel.Map.MapLevelD]
IsLvlMapD.shift_Add_iff [lemma, in DeBrLevel.Map.MapLevelD]
IsLvlMapD.shift_eq_iff [lemma, in DeBrLevel.Map.MapLevelD]
IsLvlMapD.shift_Empty_iff [lemma, in DeBrLevel.Map.MapLevelD]
IsLvlMapD.shift_find_iff [lemma, in DeBrLevel.Map.MapLevelD]
IsLvlMapD.shift_notin_iff [lemma, in DeBrLevel.Map.MapLevelD]
IsLvlMapD.shift_in_iff [lemma, in DeBrLevel.Map.MapLevelD]
IsLvlMapD.shift_in_2 [lemma, in DeBrLevel.Map.MapLevelD]
IsLvlMapD.shift_in_1 [lemma, in DeBrLevel.Map.MapLevelD]
IsLvlMapD.shift_Add [lemma, in DeBrLevel.Map.MapLevelD]
IsLvlMapD.shift_add [lemma, in DeBrLevel.Map.MapLevelD]
IsLvlMapD.shift_add_notin [lemma, in DeBrLevel.Map.MapLevelD]
IsLvlMapD.shift_Empty [lemma, in DeBrLevel.Map.MapLevelD]
IsLvlMapD.shift_eq [instance, in DeBrLevel.Map.MapLevelD]
IsLvlMapD.shift_diamond [lemma, in DeBrLevel.Map.MapLevelD]
IsLvlMapD.shift_proper [instance, in DeBrLevel.Map.MapLevelD]
IsLvlMapD.shift_func [definition, in DeBrLevel.Map.MapLevelD]
IsLvlMapD.Wf [definition, in DeBrLevel.Map.MapLevelD]
IsLvlMapD.Wf_weakening [lemma, in DeBrLevel.Map.MapLevelD]
IsLvlMapD.Wf_update [lemma, in DeBrLevel.Map.MapLevelD]
IsLvlMapD.Wf_find [lemma, in DeBrLevel.Map.MapLevelD]
IsLvlMapD.Wf_Add [lemma, in DeBrLevel.Map.MapLevelD]
IsLvlMapD.Wf_add [lemma, in DeBrLevel.Map.MapLevelD]
IsLvlMapD.Wf_add_in [lemma, in DeBrLevel.Map.MapLevelD]
IsLvlMapD.Wf_add_notin [lemma, in DeBrLevel.Map.MapLevelD]
IsLvlMapD.Wf_iff [instance, in DeBrLevel.Map.MapLevelD]
IsLvlMapD.Wf_Add_iff [lemma, in DeBrLevel.Map.MapLevelD]
IsLvlMapD.Wf_empty [lemma, in DeBrLevel.Map.MapLevelD]
IsLvlMapD.Wf_Empty_iff [lemma, in DeBrLevel.Map.MapLevelD]
IsLvlMapD.Wf_Empty [lemma, in DeBrLevel.Map.MapLevelD]
IsLvlMapD.Wf_func_iff [instance, in DeBrLevel.Map.MapLevelD]
IsLvlMapD.Wf_func_diamond [lemma, in DeBrLevel.Map.MapLevelD]
IsLvlMapD.Wf_func [definition, in DeBrLevel.Map.MapLevelD]
IsLvlMapK [module, in DeBrLevel.Map.MapLevelK]
IsLvlMapKD [module, in DeBrLevel.Map.MapLevelKD]
IsLvlMapKDInterface [module, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKDInterface.specs [section, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKDInterface.specs.k [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKDInterface.specs.m [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKDInterface.specs.m' [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKDInterface.specs.n [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKDInterface.specs.p [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKDInterface.specs.shift_find_e_1 [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKDInterface.specs.shift_find_e [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKDInterface.specs.shift_find_iff [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKDInterface.specs.shift_notin_iff [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKDInterface.specs.shift_in_iff [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKDInterface.specs.shift_in_e [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKDInterface.specs.shift_remove [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKDInterface.specs.shift_Add_iff [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKDInterface.specs.shift_Add [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKDInterface.specs.shift_add [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKDInterface.specs.shift_Empty [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKDInterface.specs.shift_Empty_iff [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKDInterface.specs.v [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKDInterface.specs.Wf_update [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKDInterface.specs.Wf_in [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKDInterface.specs.Wf_find [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKDInterface.specs.Wf_Add [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKDInterface.specs.Wf_Add_iff [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKDInterface.specs.Wf_add_in [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKDInterface.specs.Wf_add_notin [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKDInterface.specs.Wf_add [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKDInterface.specs.Wf_empty [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKDInterface.specs.Wf_Empty_iff [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKDInterface.specs.Wf_Empty [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKDInterface.specs.x [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKD.iff_equiv [instance, in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.logic_eq_equiv [instance, in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift [definition, in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_preserves_wf_zero [lemma, in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_preserves_wf [lemma, in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_preserves_wf_2 [lemma, in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_preserves_wf_gen [lemma, in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_preserves_wf_1 [lemma, in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_unfold_1 [lemma, in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_unfold [lemma, in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_permute [lemma, in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_trans [lemma, in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_zero_refl [lemma, in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_remove [lemma, in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_Add_iff [lemma, in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_find_e_1 [lemma, in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_in_e [lemma, in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_eq_iff [lemma, in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_find_e [lemma, in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_find_iff [lemma, in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_find_2 [lemma, in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_find_1 [lemma, in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_notin_iff [lemma, in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_in_iff [lemma, in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_in_2 [lemma, in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_in_1 [lemma, in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_Add [lemma, in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_add [lemma, in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_Add_2 [lemma, in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_add_notin [lemma, in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_eq [instance, in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_Empty_iff [lemma, in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_Add_1 [lemma, in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_Empty [lemma, in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_diamond [lemma, in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_proper [instance, in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_func [definition, in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.Wf [definition, in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.Wf_weakening [lemma, in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.Wf_update [lemma, in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.Wf_Add [lemma, in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.Wf_add_in [lemma, in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.Wf_in [lemma, in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.Wf_find [lemma, in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.Wf_add [lemma, in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.Wf_iff [instance, in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.Wf_Add_iff [lemma, in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.Wf_add_notin [lemma, in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.Wf_empty [lemma, in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.Wf_Empty_iff [lemma, in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.Wf_Empty [lemma, in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.Wf_func_iff [instance, in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.Wf_func_diamond [lemma, in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.Wf_func [definition, in DeBrLevel.Map.MapLevelKD]
IsLvlMapKInterface [module, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKInterface.specs [section, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKInterface.specs.k [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKInterface.specs.m [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKInterface.specs.m' [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKInterface.specs.n [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKInterface.specs.p [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKInterface.specs.shift_find [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKInterface.specs.shift_notin_iff [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKInterface.specs.shift_in_iff [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKInterface.specs.shift_in_e [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKInterface.specs.shift_remove [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKInterface.specs.shift_Add_iff [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKInterface.specs.shift_Add [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKInterface.specs.shift_add [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKInterface.specs.shift_Empty [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKInterface.specs.shift_Empty_iff [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKInterface.specs.v [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKInterface.specs.Wf_in [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKInterface.specs.Wf_Add_iff [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKInterface.specs.Wf_add_in [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKInterface.specs.Wf_add_iff [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKInterface.specs.Wf_empty [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKInterface.specs.Wf_Empty_iff [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKInterface.specs.Wf_Empty [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKInterface.specs.x [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapK.iff_equiv [instance, in DeBrLevel.Map.MapLevelK]
IsLvlMapK.logic_eq_equiv [instance, in DeBrLevel.Map.MapLevelK]
IsLvlMapK.shift [definition, in DeBrLevel.Map.MapLevelK]
IsLvlMapK.shift_preserves_wf_zero [lemma, in DeBrLevel.Map.MapLevelK]
IsLvlMapK.shift_preserves_wf [lemma, in DeBrLevel.Map.MapLevelK]
IsLvlMapK.shift_preserves_wf_2 [lemma, in DeBrLevel.Map.MapLevelK]
IsLvlMapK.shift_preserves_wf_gen [lemma, in DeBrLevel.Map.MapLevelK]
IsLvlMapK.shift_preserves_wf_1 [lemma, in DeBrLevel.Map.MapLevelK]
IsLvlMapK.shift_unfold_1 [lemma, in DeBrLevel.Map.MapLevelK]
IsLvlMapK.shift_unfold [lemma, in DeBrLevel.Map.MapLevelK]
IsLvlMapK.shift_permute [lemma, in DeBrLevel.Map.MapLevelK]
IsLvlMapK.shift_trans [lemma, in DeBrLevel.Map.MapLevelK]
IsLvlMapK.shift_zero_refl [lemma, in DeBrLevel.Map.MapLevelK]
IsLvlMapK.shift_remove [lemma, in DeBrLevel.Map.MapLevelK]
IsLvlMapK.shift_Add_iff [lemma, in DeBrLevel.Map.MapLevelK]
IsLvlMapK.shift_eq_iff [lemma, in DeBrLevel.Map.MapLevelK]
IsLvlMapK.shift_in_e [lemma, in DeBrLevel.Map.MapLevelK]
IsLvlMapK.shift_notin_iff [lemma, in DeBrLevel.Map.MapLevelK]
IsLvlMapK.shift_in_iff [lemma, in DeBrLevel.Map.MapLevelK]
IsLvlMapK.shift_in_2 [lemma, in DeBrLevel.Map.MapLevelK]
IsLvlMapK.shift_in_1 [lemma, in DeBrLevel.Map.MapLevelK]
IsLvlMapK.shift_find [lemma, in DeBrLevel.Map.MapLevelK]
IsLvlMapK.shift_Add [lemma, in DeBrLevel.Map.MapLevelK]
IsLvlMapK.shift_add [lemma, in DeBrLevel.Map.MapLevelK]
IsLvlMapK.shift_add_notin [lemma, in DeBrLevel.Map.MapLevelK]
IsLvlMapK.shift_eq [instance, in DeBrLevel.Map.MapLevelK]
IsLvlMapK.shift_Add_2 [lemma, in DeBrLevel.Map.MapLevelK]
IsLvlMapK.shift_Add_1 [lemma, in DeBrLevel.Map.MapLevelK]
IsLvlMapK.shift_Empty_iff [lemma, in DeBrLevel.Map.MapLevelK]
IsLvlMapK.shift_Empty [lemma, in DeBrLevel.Map.MapLevelK]
IsLvlMapK.shift_diamond [lemma, in DeBrLevel.Map.MapLevelK]
IsLvlMapK.shift_proper [instance, in DeBrLevel.Map.MapLevelK]
IsLvlMapK.shift_func [definition, in DeBrLevel.Map.MapLevelK]
IsLvlMapK.Wf [definition, in DeBrLevel.Map.MapLevelK]
IsLvlMapK.Wf_weakening [lemma, in DeBrLevel.Map.MapLevelK]
IsLvlMapK.Wf_in [lemma, in DeBrLevel.Map.MapLevelK]
IsLvlMapK.Wf_Add_iff [lemma, in DeBrLevel.Map.MapLevelK]
IsLvlMapK.Wf_add_iff [lemma, in DeBrLevel.Map.MapLevelK]
IsLvlMapK.Wf_add_in [lemma, in DeBrLevel.Map.MapLevelK]
IsLvlMapK.Wf_iff [instance, in DeBrLevel.Map.MapLevelK]
IsLvlMapK.Wf_add_notin [lemma, in DeBrLevel.Map.MapLevelK]
IsLvlMapK.Wf_Add [lemma, in DeBrLevel.Map.MapLevelK]
IsLvlMapK.Wf_empty [lemma, in DeBrLevel.Map.MapLevelK]
IsLvlMapK.Wf_Empty_iff [lemma, in DeBrLevel.Map.MapLevelK]
IsLvlMapK.Wf_Empty [lemma, in DeBrLevel.Map.MapLevelK]
IsLvlMapK.WF_func_iff [instance, in DeBrLevel.Map.MapLevelK]
IsLvlMapK.Wf_func_diamond [lemma, in DeBrLevel.Map.MapLevelK]
IsLvlMapK.Wf_func [definition, in DeBrLevel.Map.MapLevelK]
IsLvlMapLVL [module, in DeBrLevel.Map.MapLevelLvl]
IsLvlMapLVLD [module, in DeBrLevel.Map.MapLevelLVLD]
IsLvlMapLVLDInterface [module, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLDInterface.props [section, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLDInterface.props.k [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLDInterface.props.m [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLDInterface.props.n [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLDInterface.props.shift_new_key_le [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLDInterface.props.shift_max_key_le [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLDInterface.props.shift_max_key_gt_iff [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLDInterface.props.shift_max_refl [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLDInterface.props.shift_new_refl [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLDInterface.props.shift_new_notin [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLDInterface.props.shift_in_new_key [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLDInterface.props.shift_find_Wf [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLDInterface.props.t [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLDInterface.props.t' [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLDInterface.props.Wf_in_iff [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLDInterface.props.x [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLD.shift_in_new_key [lemma, in DeBrLevel.Map.MapLevelLVLD]
IsLvlMapLVLD.shift_find_Wf [lemma, in DeBrLevel.Map.MapLevelLVLD]
IsLvlMapLVLD.shift_new_key_le [lemma, in DeBrLevel.Map.MapLevelLVLD]
IsLvlMapLVLD.shift_max_key_le [lemma, in DeBrLevel.Map.MapLevelLVLD]
IsLvlMapLVLD.shift_max_key_gt_iff [lemma, in DeBrLevel.Map.MapLevelLVLD]
IsLvlMapLVLD.shift_new_refl [lemma, in DeBrLevel.Map.MapLevelLVLD]
IsLvlMapLVLD.shift_max_refl [lemma, in DeBrLevel.Map.MapLevelLVLD]
IsLvlMapLVLD.shift_new_notin [lemma, in DeBrLevel.Map.MapLevelLVLD]
IsLvlMapLVLD.Wf_in_iff [lemma, in DeBrLevel.Map.MapLevelLVLD]
IsLvlMapLVLInterface [module, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLInterface.specs [section, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLInterface.specs.k [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLInterface.specs.m [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLInterface.specs.n [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLInterface.specs.shift_new_key_le [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLInterface.specs.shift_max_key_le [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLInterface.specs.shift_max_key_gt_iff [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLInterface.specs.shift_max_refl [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLInterface.specs.shift_new_refl [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLInterface.specs.shift_new_notin [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLInterface.specs.shift_find_Wf [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLInterface.specs.shift_in_new_key [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLInterface.specs.t [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLInterface.specs.t' [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLInterface.specs.Wf_in_iff [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLInterface.specs.x [variable, in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVL.shift_in_new_key [lemma, in DeBrLevel.Map.MapLevelLvl]
IsLvlMapLVL.shift_find_Wf [lemma, in DeBrLevel.Map.MapLevelLvl]
IsLvlMapLVL.shift_new_key_le [lemma, in DeBrLevel.Map.MapLevelLvl]
IsLvlMapLVL.shift_max_key_le [lemma, in DeBrLevel.Map.MapLevelLvl]
IsLvlMapLVL.shift_max_key_gt_iff [lemma, in DeBrLevel.Map.MapLevelLvl]
IsLvlMapLVL.shift_new_refl [lemma, in DeBrLevel.Map.MapLevelLvl]
IsLvlMapLVL.shift_max_refl [lemma, in DeBrLevel.Map.MapLevelLvl]
IsLvlMapLVL.shift_new_notin [lemma, in DeBrLevel.Map.MapLevelLvl]
IsLvlMapLVL.Wf_in_iff [lemma, in DeBrLevel.Map.MapLevelLvl]
IsLvlOptET [module, in DeBrLevel.Datatype.OptionLevel]
IsLvlOptETWL [module, in DeBrLevel.Datatype.OptionLevel]
IsLvlOptETWL.eq_leibniz [lemma, in DeBrLevel.Datatype.OptionLevel]
IsLvlOptET.definition [section, in DeBrLevel.Datatype.OptionLevel]
IsLvlOptET.eq [definition, in DeBrLevel.Datatype.OptionLevel]
IsLvlOptET.eq_equiv [instance, in DeBrLevel.Datatype.OptionLevel]
IsLvlOptET.eq_trans [instance, in DeBrLevel.Datatype.OptionLevel]
IsLvlOptET.eq_sym [instance, in DeBrLevel.Datatype.OptionLevel]
IsLvlOptET.eq_refl [instance, in DeBrLevel.Datatype.OptionLevel]
IsLvlOptET.shift [section, in DeBrLevel.Datatype.OptionLevel]
IsLvlOptET.shift [definition, in DeBrLevel.Datatype.OptionLevel]
IsLvlOptET.shift_preserves_wf_zero [lemma, in DeBrLevel.Datatype.OptionLevel]
IsLvlOptET.shift_preserves_wf_2 [lemma, in DeBrLevel.Datatype.OptionLevel]
IsLvlOptET.shift_preserves_wf_gen [lemma, in DeBrLevel.Datatype.OptionLevel]
IsLvlOptET.shift_preserves_wf_1 [lemma, in DeBrLevel.Datatype.OptionLevel]
IsLvlOptET.shift_preserves_wf [lemma, in DeBrLevel.Datatype.OptionLevel]
IsLvlOptET.shift_unfold_1 [lemma, in DeBrLevel.Datatype.OptionLevel]
IsLvlOptET.shift_unfold [lemma, in DeBrLevel.Datatype.OptionLevel]
IsLvlOptET.shift_permute [lemma, in DeBrLevel.Datatype.OptionLevel]
IsLvlOptET.shift_trans [lemma, in DeBrLevel.Datatype.OptionLevel]
IsLvlOptET.shift_zero_refl [lemma, in DeBrLevel.Datatype.OptionLevel]
IsLvlOptET.shift_eq_iff [lemma, in DeBrLevel.Datatype.OptionLevel]
IsLvlOptET.shift_eq [instance, in DeBrLevel.Datatype.OptionLevel]
IsLvlOptET.shift.k [variable, in DeBrLevel.Datatype.OptionLevel]
IsLvlOptET.shift.m [variable, in DeBrLevel.Datatype.OptionLevel]
IsLvlOptET.shift.n [variable, in DeBrLevel.Datatype.OptionLevel]
IsLvlOptET.shift.p [variable, in DeBrLevel.Datatype.OptionLevel]
IsLvlOptET.shift.t [variable, in DeBrLevel.Datatype.OptionLevel]
IsLvlOptET.shift.t1 [variable, in DeBrLevel.Datatype.OptionLevel]
IsLvlOptET.t [definition, in DeBrLevel.Datatype.OptionLevel]
IsLvlOptET.Wf [definition, in DeBrLevel.Datatype.OptionLevel]
IsLvlOptET.Wf_weakening [lemma, in DeBrLevel.Datatype.OptionLevel]
IsLvlOptET.Wf_iff [instance, in DeBrLevel.Datatype.OptionLevel]
IsLvlOT [module, in DeBrLevel.Core.LevelInterface]
IsLvlOTWL [module, in DeBrLevel.Core.LevelInterface]
IsLvlPairET [module, in DeBrLevel.Datatype.PairLevel]
IsLvlPairETWL [module, in DeBrLevel.Datatype.PairLevel]
IsLvlPairETWL.eq_leibniz [lemma, in DeBrLevel.Datatype.PairLevel]
IsLvlPairET.eq [definition, in DeBrLevel.Datatype.PairLevel]
IsLvlPairET.eq_equiv [instance, in DeBrLevel.Datatype.PairLevel]
IsLvlPairET.eq_trans [instance, in DeBrLevel.Datatype.PairLevel]
IsLvlPairET.eq_sym [instance, in DeBrLevel.Datatype.PairLevel]
IsLvlPairET.eq_refl [instance, in DeBrLevel.Datatype.PairLevel]
IsLvlPairET.shift [section, in DeBrLevel.Datatype.PairLevel]
IsLvlPairET.shift [definition, in DeBrLevel.Datatype.PairLevel]
IsLvlPairET.shift_preserves_wf_zero [lemma, in DeBrLevel.Datatype.PairLevel]
IsLvlPairET.shift_preserves_wf_2 [lemma, in DeBrLevel.Datatype.PairLevel]
IsLvlPairET.shift_preserves_wf_gen [lemma, in DeBrLevel.Datatype.PairLevel]
IsLvlPairET.shift_preserves_wf_1 [lemma, in DeBrLevel.Datatype.PairLevel]
IsLvlPairET.shift_preserves_wf [lemma, in DeBrLevel.Datatype.PairLevel]
IsLvlPairET.shift_unfold_1 [lemma, in DeBrLevel.Datatype.PairLevel]
IsLvlPairET.shift_unfold [lemma, in DeBrLevel.Datatype.PairLevel]
IsLvlPairET.shift_permute [lemma, in DeBrLevel.Datatype.PairLevel]
IsLvlPairET.shift_trans [lemma, in DeBrLevel.Datatype.PairLevel]
IsLvlPairET.shift_zero_refl [lemma, in DeBrLevel.Datatype.PairLevel]
IsLvlPairET.shift_eq_iff [lemma, in DeBrLevel.Datatype.PairLevel]
IsLvlPairET.shift_eq [instance, in DeBrLevel.Datatype.PairLevel]
IsLvlPairET.shift.k [variable, in DeBrLevel.Datatype.PairLevel]
IsLvlPairET.shift.m [variable, in DeBrLevel.Datatype.PairLevel]
IsLvlPairET.shift.n [variable, in DeBrLevel.Datatype.PairLevel]
IsLvlPairET.shift.p [variable, in DeBrLevel.Datatype.PairLevel]
IsLvlPairET.shift.t [variable, in DeBrLevel.Datatype.PairLevel]
IsLvlPairET.t [definition, in DeBrLevel.Datatype.PairLevel]
IsLvlPairET.Wf [definition, in DeBrLevel.Datatype.PairLevel]
IsLvlPairET.Wf_weakening [lemma, in DeBrLevel.Datatype.PairLevel]
IsLvlPairET.Wf_iff [instance, in DeBrLevel.Datatype.PairLevel]
IsLvlPairOT [module, in DeBrLevel.Datatype.PairLevel]
IsLvlPairOTWL [module, in DeBrLevel.Datatype.PairLevel]
IsLvlPairOTWL.eq_leibniz [lemma, in DeBrLevel.Datatype.PairLevel]
IsLvlPairOT.shift [section, in DeBrLevel.Datatype.PairLevel]
IsLvlPairOT.shift [definition, in DeBrLevel.Datatype.PairLevel]
IsLvlPairOT.shift_preserves_wf_zero [lemma, in DeBrLevel.Datatype.PairLevel]
IsLvlPairOT.shift_preserves_wf_2 [lemma, in DeBrLevel.Datatype.PairLevel]
IsLvlPairOT.shift_preserves_wf_gen [lemma, in DeBrLevel.Datatype.PairLevel]
IsLvlPairOT.shift_preserves_wf_1 [lemma, in DeBrLevel.Datatype.PairLevel]
IsLvlPairOT.shift_preserves_wf [lemma, in DeBrLevel.Datatype.PairLevel]
IsLvlPairOT.shift_unfold_1 [lemma, in DeBrLevel.Datatype.PairLevel]
IsLvlPairOT.shift_unfold [lemma, in DeBrLevel.Datatype.PairLevel]
IsLvlPairOT.shift_permute [lemma, in DeBrLevel.Datatype.PairLevel]
IsLvlPairOT.shift_trans [lemma, in DeBrLevel.Datatype.PairLevel]
IsLvlPairOT.shift_zero_refl [lemma, in DeBrLevel.Datatype.PairLevel]
IsLvlPairOT.shift_eq_iff [lemma, in DeBrLevel.Datatype.PairLevel]
IsLvlPairOT.shift_eq [instance, in DeBrLevel.Datatype.PairLevel]
IsLvlPairOT.shift.k [variable, in DeBrLevel.Datatype.PairLevel]
IsLvlPairOT.shift.m [variable, in DeBrLevel.Datatype.PairLevel]
IsLvlPairOT.shift.n [variable, in DeBrLevel.Datatype.PairLevel]
IsLvlPairOT.shift.p [variable, in DeBrLevel.Datatype.PairLevel]
IsLvlPairOT.shift.t [variable, in DeBrLevel.Datatype.PairLevel]
IsLvlPairOT.shift.t1 [variable, in DeBrLevel.Datatype.PairLevel]
IsLvlPairOT.Wf [definition, in DeBrLevel.Datatype.PairLevel]
IsLvlPairOT.Wf_weakening [lemma, in DeBrLevel.Datatype.PairLevel]
IsLvlPairOT.Wf_iff [instance, in DeBrLevel.Datatype.PairLevel]
IsLvlSet [module, in DeBrLevel.Set.SetLevel]
IsLvlSetInterface [module, in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.compare [definition, in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.compare_spec [definition, in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.eq [definition, in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.eq_leibniz [definition, in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.eq_dec [definition, in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.eq_equiv [definition, in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.lt [definition, in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.lt_compat [definition, in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.lt_strorder [definition, in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.specs [section, in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.specs.m [variable, in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.specs.n [variable, in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.specs.shift_notin_iff [variable, in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.specs.shift_in_e [variable, in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.specs.shift_in_iff [variable, in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.specs.shift_remove [variable, in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.specs.shift_add [variable, in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.specs.shift_add_in [variable, in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.specs.shift_add_notin [variable, in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.specs.shift_diff [variable, in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.specs.shift_inter [variable, in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.specs.shift_union [variable, in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.specs.shift_singleton [variable, in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.specs.shift_empty [variable, in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.specs.shift_Empty [variable, in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.specs.t [variable, in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.specs.t' [variable, in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.specs.v [variable, in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.specs.Wf_in [variable, in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.specs.Wf_singleton_iff [variable, in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.specs.Wf_union_iff [variable, in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.specs.Wf_empty [variable, in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.specs.Wf_add_iff [variable, in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.specs.Wf_unfold [variable, in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.t [definition, in DeBrLevel.Set.SetLevelInterface]
IsLvlSetLVLInterface [module, in DeBrLevel.Set.SetLevelInterface]
IsLvlSetLVLInterface.max_key_eq [instance, in DeBrLevel.Set.SetLevelInterface]
IsLvlSetLVLInterface.max_key [axiom, in DeBrLevel.Set.SetLevelInterface]
IsLvlSetLVLInterface.new_key_eq [instance, in DeBrLevel.Set.SetLevelInterface]
IsLvlSetLVLInterface.new_key [axiom, in DeBrLevel.Set.SetLevelInterface]
IsLvlSetLVLInterface.specifications [section, in DeBrLevel.Set.SetLevelInterface]
IsLvlSetLVLInterface.specifications.k [variable, in DeBrLevel.Set.SetLevelInterface]
IsLvlSetLVLInterface.specifications.m [variable, in DeBrLevel.Set.SetLevelInterface]
IsLvlSetLVLInterface.specifications.max_key_add_max [variable, in DeBrLevel.Set.SetLevelInterface]
IsLvlSetLVLInterface.specifications.max_key_Add_max [variable, in DeBrLevel.Set.SetLevelInterface]
IsLvlSetLVLInterface.specifications.max_key_empty [variable, in DeBrLevel.Set.SetLevelInterface]
IsLvlSetLVLInterface.specifications.max_key_Empty [variable, in DeBrLevel.Set.SetLevelInterface]
IsLvlSetLVLInterface.specifications.n [variable, in DeBrLevel.Set.SetLevelInterface]
IsLvlSetLVLInterface.specifications.new_key_in [variable, in DeBrLevel.Set.SetLevelInterface]
IsLvlSetLVLInterface.specifications.new_key_add_max [variable, in DeBrLevel.Set.SetLevelInterface]
IsLvlSetLVLInterface.specifications.new_key_Add_max [variable, in DeBrLevel.Set.SetLevelInterface]
IsLvlSetLVLInterface.specifications.new_key_empty [variable, in DeBrLevel.Set.SetLevelInterface]
IsLvlSetLVLInterface.specifications.new_key_Empty [variable, in DeBrLevel.Set.SetLevelInterface]
IsLvlSetLVLInterface.specifications.p [variable, in DeBrLevel.Set.SetLevelInterface]
IsLvlSetLVLInterface.specifications.s [variable, in DeBrLevel.Set.SetLevelInterface]
IsLvlSetLVLInterface.specifications.shift_new_refl [variable, in DeBrLevel.Set.SetLevelInterface]
IsLvlSetLVLInterface.specifications.shift_permute_2 [variable, in DeBrLevel.Set.SetLevelInterface]
IsLvlSetLVLInterface.specifications.shift_permute_1 [variable, in DeBrLevel.Set.SetLevelInterface]
IsLvlSetLVLInterface.specifications.s' [variable, in DeBrLevel.Set.SetLevelInterface]
IsLvlSetLVLInterface.specifications.v [variable, in DeBrLevel.Set.SetLevelInterface]
IsLvlSet.compare [definition, in DeBrLevel.Set.SetLevel]
IsLvlSet.compare_spec [definition, in DeBrLevel.Set.SetLevel]
IsLvlSet.eq [definition, in DeBrLevel.Set.SetLevel]
IsLvlSet.eq_leibniz [definition, in DeBrLevel.Set.SetLevel]
IsLvlSet.eq_dec [definition, in DeBrLevel.Set.SetLevel]
IsLvlSet.eq_equiv [definition, in DeBrLevel.Set.SetLevel]
IsLvlSet.lt [definition, in DeBrLevel.Set.SetLevel]
IsLvlSet.lt_compat [definition, in DeBrLevel.Set.SetLevel]
IsLvlSet.lt_strorder [definition, in DeBrLevel.Set.SetLevel]
IsLvlSet.shift [definition, in DeBrLevel.Set.SetLevel]
IsLvlSet.shift_preserves_wf_2 [lemma, in DeBrLevel.Set.SetLevel]
IsLvlSet.shift_preserves_wf_gen [lemma, in DeBrLevel.Set.SetLevel]
IsLvlSet.shift_preserves_wf_zero [lemma, in DeBrLevel.Set.SetLevel]
IsLvlSet.shift_preserves_wf [lemma, in DeBrLevel.Set.SetLevel]
IsLvlSet.shift_preserves_wf_1 [lemma, in DeBrLevel.Set.SetLevel]
IsLvlSet.shift_unfold_1 [lemma, in DeBrLevel.Set.SetLevel]
IsLvlSet.shift_unfold [lemma, in DeBrLevel.Set.SetLevel]
IsLvlSet.shift_permute [lemma, in DeBrLevel.Set.SetLevel]
IsLvlSet.shift_trans [lemma, in DeBrLevel.Set.SetLevel]
IsLvlSet.shift_eq [instance, in DeBrLevel.Set.SetLevel]
IsLvlSet.shift_zero_refl [lemma, in DeBrLevel.Set.SetLevel]
IsLvlSet.shift_diff [lemma, in DeBrLevel.Set.SetLevel]
IsLvlSet.shift_inter [lemma, in DeBrLevel.Set.SetLevel]
IsLvlSet.shift_eq_iff [lemma, in DeBrLevel.Set.SetLevel]
IsLvlSet.shift_remove [lemma, in DeBrLevel.Set.SetLevel]
IsLvlSet.shift_notin_iff [lemma, in DeBrLevel.Set.SetLevel]
IsLvlSet.shift_in_e [lemma, in DeBrLevel.Set.SetLevel]
IsLvlSet.shift_add [lemma, in DeBrLevel.Set.SetLevel]
IsLvlSet.shift_in_iff [lemma, in DeBrLevel.Set.SetLevel]
IsLvlSet.shift_add_in [lemma, in DeBrLevel.Set.SetLevel]
IsLvlSet.shift_add_notin [lemma, in DeBrLevel.Set.SetLevel]
IsLvlSet.shift_singleton [lemma, in DeBrLevel.Set.SetLevel]
IsLvlSet.shift_empty [lemma, in DeBrLevel.Set.SetLevel]
IsLvlSet.shift_Empty [lemma, in DeBrLevel.Set.SetLevel]
IsLvlSet.shift_union [lemma, in DeBrLevel.Set.SetLevel]
IsLvlSet.specs [section, in DeBrLevel.Set.SetLevel]
IsLvlSet.specs.k [variable, in DeBrLevel.Set.SetLevel]
IsLvlSet.specs.m [variable, in DeBrLevel.Set.SetLevel]
IsLvlSet.specs.n [variable, in DeBrLevel.Set.SetLevel]
IsLvlSet.specs.s [variable, in DeBrLevel.Set.SetLevel]
IsLvlSet.specs.s' [variable, in DeBrLevel.Set.SetLevel]
IsLvlSet.specs.v [variable, in DeBrLevel.Set.SetLevel]
IsLvlSet.t [definition, in DeBrLevel.Set.SetLevel]
IsLvlSet.Wf [definition, in DeBrLevel.Set.SetLevel]
IsLvlSet.Wf_weakening [lemma, in DeBrLevel.Set.SetLevel]
IsLvlSet.Wf_in [lemma, in DeBrLevel.Set.SetLevel]
IsLvlSet.Wf_singleton_iff [lemma, in DeBrLevel.Set.SetLevel]
IsLvlSet.Wf_union_iff [lemma, in DeBrLevel.Set.SetLevel]
IsLvlSet.Wf_empty [lemma, in DeBrLevel.Set.SetLevel]
IsLvlSet.Wf_add_iff [lemma, in DeBrLevel.Set.SetLevel]
IsLvlSet.Wf_unfold [lemma, in DeBrLevel.Set.SetLevel]
IsLvlSet.Wf_iff [instance, in DeBrLevel.Set.SetLevel]
IsWF [module, in DeBrLevel.Core.LevelInterface]
IsWFb [module, in DeBrLevel.Core.LevelInterface]
IsWFb.is_wf_eq [instance, in DeBrLevel.Core.LevelInterface]
IsWFb.is_wf [axiom, in DeBrLevel.Core.LevelInterface]
IsWFFull [module, in DeBrLevel.Core.LevelInterface]
IsWFFull.specs [section, in DeBrLevel.Core.LevelInterface]
IsWFFull.specs.k [variable, in DeBrLevel.Core.LevelInterface]
IsWFFull.specs.notWf_is_wf_false [variable, in DeBrLevel.Core.LevelInterface]
IsWFFull.specs.t [variable, in DeBrLevel.Core.LevelInterface]
IsWFFull.specs.Wf_is_wf_true [variable, in DeBrLevel.Core.LevelInterface]
IsWF.Wf [axiom, in DeBrLevel.Core.LevelInterface]
IsWF.Wf_iff [instance, in DeBrLevel.Core.LevelInterface]
IsWF.Wf_weakening [axiom, in DeBrLevel.Core.LevelInterface]
L
Level [module, in DeBrLevel.Core.Level]Level [library]
LevelInterface [library]
Levels [module, in DeBrLevel.Set.Levels]
Levels [library]
Levels.logic_eq [instance, in DeBrLevel.Set.Levels]
Levels.max_key_Add_max [lemma, in DeBrLevel.Set.Levels]
Levels.max_key_add_max [lemma, in DeBrLevel.Set.Levels]
Levels.max_key_empty [lemma, in DeBrLevel.Set.Levels]
Levels.max_key_Empty [lemma, in DeBrLevel.Set.Levels]
Levels.max_key_eq [instance, in DeBrLevel.Set.Levels]
Levels.max_transpose [lemma, in DeBrLevel.Set.Levels]
Levels.max_eq [instance, in DeBrLevel.Set.Levels]
Levels.max_key [definition, in DeBrLevel.Set.Levels]
Levels.new_key_in [lemma, in DeBrLevel.Set.Levels]
Levels.new_key_Add_max [lemma, in DeBrLevel.Set.Levels]
Levels.new_key_add_max [lemma, in DeBrLevel.Set.Levels]
Levels.new_key_empty [lemma, in DeBrLevel.Set.Levels]
Levels.new_key_Empty [lemma, in DeBrLevel.Set.Levels]
Levels.new_key_eq [instance, in DeBrLevel.Set.Levels]
Levels.new_key [definition, in DeBrLevel.Set.Levels]
Levels.shift_new_refl [lemma, in DeBrLevel.Set.Levels]
Levels.shift_permute_2 [lemma, in DeBrLevel.Set.Levels]
Levels.shift_permute_1 [lemma, in DeBrLevel.Set.Levels]
Level.eq_leibniz [lemma, in DeBrLevel.Core.Level]
Level.gt_neq_nlt [lemma, in DeBrLevel.Core.Level]
Level.is_wf_eq [instance, in DeBrLevel.Core.Level]
Level.is_wf [definition, in DeBrLevel.Core.Level]
Level.lt_not_eq [lemma, in DeBrLevel.Core.Level]
Level.lt_eq.t2 [variable, in DeBrLevel.Core.Level]
Level.lt_eq.t1 [variable, in DeBrLevel.Core.Level]
Level.lt_eq [section, in DeBrLevel.Core.Level]
Level.notWf_is_wf_false [lemma, in DeBrLevel.Core.Level]
Level.shift [section, in DeBrLevel.Core.Level]
Level.shift [definition, in DeBrLevel.Core.Level]
Level.shift_preserves_wf_zero [lemma, in DeBrLevel.Core.Level]
Level.shift_preserves_wf_2 [lemma, in DeBrLevel.Core.Level]
Level.shift_preserves_wf_gen [lemma, in DeBrLevel.Core.Level]
Level.shift_preserves_wf_1 [lemma, in DeBrLevel.Core.Level]
Level.shift_preserves_wf [lemma, in DeBrLevel.Core.Level]
Level.shift_le [lemma, in DeBrLevel.Core.Level]
Level.shift_gt_iff [lemma, in DeBrLevel.Core.Level]
Level.shift_unfold_1 [lemma, in DeBrLevel.Core.Level]
Level.shift_unfold [lemma, in DeBrLevel.Core.Level]
Level.shift_permute_2 [lemma, in DeBrLevel.Core.Level]
Level.shift_permute_1 [lemma, in DeBrLevel.Core.Level]
Level.shift_permute [lemma, in DeBrLevel.Core.Level]
Level.shift_trans [lemma, in DeBrLevel.Core.Level]
Level.shift_wf_refl [lemma, in DeBrLevel.Core.Level]
Level.shift_zero_refl [lemma, in DeBrLevel.Core.Level]
Level.shift_eq_iff [lemma, in DeBrLevel.Core.Level]
Level.shift_neq_1 [lemma, in DeBrLevel.Core.Level]
Level.shift_neq [lemma, in DeBrLevel.Core.Level]
Level.shift_eq [instance, in DeBrLevel.Core.Level]
Level.shift.k [variable, in DeBrLevel.Core.Level]
Level.shift.m [variable, in DeBrLevel.Core.Level]
Level.shift.n [variable, in DeBrLevel.Core.Level]
Level.shift.p [variable, in DeBrLevel.Core.Level]
Level.shift.t [variable, in DeBrLevel.Core.Level]
Level.shift.t1 [variable, in DeBrLevel.Core.Level]
Level.Wf [definition, in DeBrLevel.Core.Level]
Level.Wf_weakening [lemma, in DeBrLevel.Core.Level]
Level.Wf_iff [instance, in DeBrLevel.Core.Level]
Level.Wf_is_wf_true [lemma, in DeBrLevel.Core.Level]
ListLevel [library]
Lvl [module, in DeBrLevel.Core.LevelInterface]
M
MakeBdlLvlFullSet [module, in DeBrLevel.Set.SetLevel]MakeBdlLvlFullSet.St [module, in DeBrLevel.Set.SetLevel]
MakeBdlLvlMapD [module, in DeBrLevel.Map.MapLevelD]
MakeBdlLvlMapD.Ext [module, in DeBrLevel.Map.MapLevelD]
MakeBdlLvlMapD.Raw [module, in DeBrLevel.Map.MapLevelD]
MakeBdlLvlMapK [module, in DeBrLevel.Map.MapLevelK]
MakeBdlLvlMapKD [module, in DeBrLevel.Map.MapLevelKD]
MakeBdlLvlMapKD.Ext [module, in DeBrLevel.Map.MapLevelKD]
MakeBdlLvlMapKD.Raw [module, in DeBrLevel.Map.MapLevelKD]
MakeBdlLvlMapK.Ext [module, in DeBrLevel.Map.MapLevelK]
MakeBdlLvlMapK.Raw [module, in DeBrLevel.Map.MapLevelK]
MakeBdlLvlMapLVL [module, in DeBrLevel.Map.MapLevelLvl]
MakeBdlLvlMapLVLD [module, in DeBrLevel.Map.MapLevelLVLD]
MakeBdlLvlMapLVLD.Ext [module, in DeBrLevel.Map.MapLevelLVLD]
MakeBdlLvlMapLVLD.Raw [module, in DeBrLevel.Map.MapLevelLVLD]
MakeBdlLvlMapLVL.Ext [module, in DeBrLevel.Map.MapLevelLvl]
MakeBdlLvlMapLVL.Raw [module, in DeBrLevel.Map.MapLevelLvl]
MakeBdlLvlSet [module, in DeBrLevel.Set.SetLevel]
MakeBdlLvlSet.St [module, in DeBrLevel.Set.SetLevel]
MakeLVL [module, in DeBrLevel.Set.Levels]
MakeLvlFullSet [module, in DeBrLevel.Set.SetLevel]
MakeLvlFullSet.St [module, in DeBrLevel.Set.SetLevel]
MakeLvlMapD [module, in DeBrLevel.Map.MapLevelD]
MakeLvlMapD.Ext [module, in DeBrLevel.Map.MapLevelD]
MakeLvlMapD.Raw [module, in DeBrLevel.Map.MapLevelD]
MakeLvlMapK [module, in DeBrLevel.Map.MapLevelK]
MakeLvlMapKD [module, in DeBrLevel.Map.MapLevelKD]
MakeLvlMapKD.Ext [module, in DeBrLevel.Map.MapLevelKD]
MakeLvlMapKD.Raw [module, in DeBrLevel.Map.MapLevelKD]
MakeLvlMapK.Ext [module, in DeBrLevel.Map.MapLevelK]
MakeLvlMapK.Raw [module, in DeBrLevel.Map.MapLevelK]
MakeLvlMapLVL [module, in DeBrLevel.Map.MapLevelLvl]
MakeLvlMapLVLD [module, in DeBrLevel.Map.MapLevelLVLD]
MakeLvlMapLVLD.Ext [module, in DeBrLevel.Map.MapLevelLVLD]
MakeLvlMapLVLD.Raw [module, in DeBrLevel.Map.MapLevelLVLD]
MakeLvlMapLVL.Ext [module, in DeBrLevel.Map.MapLevelLvl]
MakeLvlMapLVL.Raw [module, in DeBrLevel.Map.MapLevelLvl]
MakeLvlSet [module, in DeBrLevel.Set.SetLevel]
MakeLvlSet.St [module, in DeBrLevel.Set.SetLevel]
MakeLVL.St [module, in DeBrLevel.Set.Levels]
MapET [module, in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL [module, in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.max_key_add_in [lemma, in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.max_key_Submap [lemma, in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.max_key_in [lemma, in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.max_key_add_max_key [lemma, in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.max_key_notin [lemma, in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.max_key_ub [lemma, in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.max_key_add_iff [lemma, in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.max_key_add_r [lemma, in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.max_key_add_l [lemma, in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.max_key_add_max [lemma, in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.max_key_Add_r [lemma, in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.max_key_Add_l [lemma, in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.max_key_Add_max [lemma, in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.max_key_empty [lemma, in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.max_key_Empty [lemma, in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.max_key_eq [instance, in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.max_key_diamond [lemma, in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.max_key_proper_forall [instance, in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.max_key_proper [instance, in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.max_key [definition, in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.new_key_Submap_add [lemma, in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.new_key_Submap [lemma, in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.new_key_in [lemma, in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.new_key_notin [lemma, in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.new_key_add_new_key [lemma, in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.new_key_Add_r [lemma, in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.new_key_Add_l [lemma, in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.new_key_add_in [lemma, in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.new_key_add_r [lemma, in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.new_key_add_l [lemma, in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.new_key_geq_max_key [lemma, in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.new_key_add_max [lemma, in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.new_key_Add_max [lemma, in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.new_key_empty [lemma, in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.new_key_Empty [lemma, in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.new_key_eq [instance, in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.new_key_unfold [lemma, in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.new_key [definition, in DeBrLevel.Map.Mapkit.MapExt]
MapET.add_shadow [lemma, in DeBrLevel.Map.Mapkit.MapExt]
MapET.add_remove [lemma, in DeBrLevel.Map.Mapkit.MapExt]
MapET.Add_eq_iff [instance, in DeBrLevel.Map.Mapkit.MapExt]
MapET.Empty_eq [lemma, in DeBrLevel.Map.Mapkit.MapExt]
MapET.Empty_eq_iff [instance, in DeBrLevel.Map.Mapkit.MapExt]
MapET.eq [definition, in DeBrLevel.Map.Mapkit.MapExt]
MapET.eq_equiv [instance, in DeBrLevel.Map.Mapkit.MapExt]
MapET.For_all_add_notin [lemma, in DeBrLevel.Map.Mapkit.MapExt]
MapET.For_all_add [lemma, in DeBrLevel.Map.Mapkit.MapExt]
MapET.For_all_Empty [lemma, in DeBrLevel.Map.Mapkit.MapExt]
MapET.For_all_empty [lemma, in DeBrLevel.Map.Mapkit.MapExt]
MapET.For_all_proper [instance, in DeBrLevel.Map.Mapkit.MapExt]
MapET.For_all [definition, in DeBrLevel.Map.Mapkit.MapExt]
MapET.iff_equiv [instance, in DeBrLevel.Map.Mapkit.MapExt]
MapET.is_empty_add [lemma, in DeBrLevel.Map.Mapkit.MapExt]
MapET.is_empty_Add [lemma, in DeBrLevel.Map.Mapkit.MapExt]
MapET.logic_eq_equiv [instance, in DeBrLevel.Map.Mapkit.MapExt]
MapET.notEmpty_find [lemma, in DeBrLevel.Map.Mapkit.MapExt]
MapET.notEmpty_Add [lemma, in DeBrLevel.Map.Mapkit.MapExt]
MapET.OP [module, in DeBrLevel.Map.Mapkit.MapExt]
MapET.Submap [definition, in DeBrLevel.Map.Mapkit.MapExt]
MapET.Submap_po [instance, in DeBrLevel.Map.Mapkit.MapExt]
MapET.Submap_trans [instance, in DeBrLevel.Map.Mapkit.MapExt]
MapET.Submap_eq [instance, in DeBrLevel.Map.Mapkit.MapExt]
MapET.Submap_refl [instance, in DeBrLevel.Map.Mapkit.MapExt]
MapET.Submap_find [lemma, in DeBrLevel.Map.Mapkit.MapExt]
MapET.Submap_notin [lemma, in DeBrLevel.Map.Mapkit.MapExt]
MapET.Submap_in [lemma, in DeBrLevel.Map.Mapkit.MapExt]
MapET.Submap_add_2 [lemma, in DeBrLevel.Map.Mapkit.MapExt]
MapET.Submap_add_1 [lemma, in DeBrLevel.Map.Mapkit.MapExt]
MapET.Submap_add [lemma, in DeBrLevel.Map.Mapkit.MapExt]
MapET.Submap_Add_1 [lemma, in DeBrLevel.Map.Mapkit.MapExt]
MapET.Submap_Add_find [lemma, in DeBrLevel.Map.Mapkit.MapExt]
MapET.Submap_Add_in [lemma, in DeBrLevel.Map.Mapkit.MapExt]
MapET.Submap_Add [lemma, in DeBrLevel.Map.Mapkit.MapExt]
MapET.Submap_empty_bot [lemma, in DeBrLevel.Map.Mapkit.MapExt]
MapET.Submap_Empty [lemma, in DeBrLevel.Map.Mapkit.MapExt]
MapET.Submap_Empty_bot [lemma, in DeBrLevel.Map.Mapkit.MapExt]
MapET.t [definition, in DeBrLevel.Map.Mapkit.MapExt]
MapExt [library]
MapExtInterface [library]
MapInterface [module, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.Add_eq_iff [instance, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.Empty_eq_iff [instance, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.eq [definition, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.eq_equiv [instance, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.For_all_proper [instance, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.For_all [axiom, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.OP [module, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.specifications [section, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.specifications.add_remove [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.specifications.add_shadow [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.specifications.e [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.specifications.Empty_eq [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.specifications.e' [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.specifications.For_all_add_notin [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.specifications.For_all_add [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.specifications.For_all_Empty [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.specifications.For_all_empty [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.specifications.is_empty_add [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.specifications.is_empty_Add [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.specifications.m [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.specifications.m' [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.specifications.m1 [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.specifications.notEmpty_find [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.specifications.notEmpty_Add [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.specifications.P [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.specifications.Submap_find [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.specifications.Submap_notin [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.specifications.Submap_in [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.specifications.Submap_add_1 [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.specifications.Submap_add_2 [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.specifications.Submap_add [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.specifications.Submap_Add_1 [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.specifications.Submap_Add_find [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.specifications.Submap_Add_in [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.specifications.Submap_Add [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.specifications.Submap_empty_bot [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.specifications.Submap_Empty [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.specifications.Submap_Empty_bot [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.specifications.x [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.Submap [axiom, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.Submap_po [instance, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.Submap_eq [instance, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.Submap_trans [instance, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.Submap_refl [instance, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.t [definition, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLevelD [library]
MapLevelInterface [library]
MapLevelK [library]
MapLevelKD [library]
MapLevelLvl [library]
MapLevelLVLD [library]
MapLVLInterface [module, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.max_key_eq [instance, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.max_key [axiom, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.new_key_eq [instance, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.new_key [axiom, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs [section, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.m [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.max_key_Submap [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.max_key_in [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.max_key_notin [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.max_key_add_max [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.max_key_add_max_key [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.max_key_add_iff [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.max_key_add_in [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.max_key_add_r [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.max_key_add_l [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.max_key_Add_max [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.max_key_Add_r [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.max_key_Add_l [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.max_key_empty [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.max_key_Empty [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.max_key_ub [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.m' [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.new_key_Submap_add [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.new_key_Submap [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.new_key_in [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.new_key_notin [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.new_key_add_new_key [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.new_key_add_in [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.new_key_add_r [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.new_key_add_l [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.new_key_add_max [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.new_key_Add_max [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.new_key_Add_r [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.new_key_Add_l [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.new_key_empty [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.new_key_Empty [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.new_key_unfold [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.new_key_geq_max_key [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.v [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.v' [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.x [variable, in DeBrLevel.Map.Mapkit.MapExtInterface]
O
OptionLevel [library]OrderedTypeWithLeibniz [module, in DeBrLevel.Core.LevelInterface]
OrderedTypeWithLeibniz.eq_leibniz [axiom, in DeBrLevel.Core.LevelInterface]
P
PairLevel [library]S
SetLevel [library]SetLevelInterface [library]
SetOTWithLeibniz [module, in DeBrLevel.Set.Setkit.SetOTwL]
SetOTWithLeibnizInterface [module, in DeBrLevel.Set.Setkit.SetOTwLInterface]
SetOTWithLeibnizInterface.ltb [axiom, in DeBrLevel.Set.Setkit.SetOTwLInterface]
SetOTWithLeibnizInterface.map [axiom, in DeBrLevel.Set.Setkit.SetOTwLInterface]
SetOTWithLeibnizInterface.proper_1 [instance, in DeBrLevel.Set.Setkit.SetOTwLInterface]
SetOTWithLeibnizInterface.specs [section, in DeBrLevel.Set.Setkit.SetOTwLInterface]
SetOTWithLeibnizInterface.specs.add_notin_spec [variable, in DeBrLevel.Set.Setkit.SetOTwLInterface]
SetOTWithLeibnizInterface.specs.add_eq_leibniz [variable, in DeBrLevel.Set.Setkit.SetOTwLInterface]
SetOTWithLeibnizInterface.specs.Add_inv [variable, in DeBrLevel.Set.Setkit.SetOTwLInterface]
SetOTWithLeibnizInterface.specs.diff_notin_spec [variable, in DeBrLevel.Set.Setkit.SetOTwLInterface]
SetOTWithLeibnizInterface.specs.diff_notin_add_spec [variable, in DeBrLevel.Set.Setkit.SetOTwLInterface]
SetOTWithLeibnizInterface.specs.diff_in_add_spec [variable, in DeBrLevel.Set.Setkit.SetOTwLInterface]
SetOTWithLeibnizInterface.specs.eqb_refl [variable, in DeBrLevel.Set.Setkit.SetOTwLInterface]
SetOTWithLeibnizInterface.specs.f [variable, in DeBrLevel.Set.Setkit.SetOTwLInterface]
SetOTWithLeibnizInterface.specs.gt_neq_nlt [variable, in DeBrLevel.Set.Setkit.SetOTwLInterface]
SetOTWithLeibnizInterface.specs.inter_notin_add_spec [variable, in DeBrLevel.Set.Setkit.SetOTwLInterface]
SetOTWithLeibnizInterface.specs.inter_in_add_spec [variable, in DeBrLevel.Set.Setkit.SetOTwLInterface]
SetOTWithLeibnizInterface.specs.ltb_lt [variable, in DeBrLevel.Set.Setkit.SetOTwLInterface]
SetOTWithLeibnizInterface.specs.map_union_spec [variable, in DeBrLevel.Set.Setkit.SetOTwLInterface]
SetOTWithLeibnizInterface.specs.map_add_in_spec [variable, in DeBrLevel.Set.Setkit.SetOTwLInterface]
SetOTWithLeibnizInterface.specs.map_add_notin_spec [variable, in DeBrLevel.Set.Setkit.SetOTwLInterface]
SetOTWithLeibnizInterface.specs.map_in_spec [variable, in DeBrLevel.Set.Setkit.SetOTwLInterface]
SetOTWithLeibnizInterface.specs.map_singleton_spec [variable, in DeBrLevel.Set.Setkit.SetOTwLInterface]
SetOTWithLeibnizInterface.specs.map_empty_spec [variable, in DeBrLevel.Set.Setkit.SetOTwLInterface]
SetOTWithLeibnizInterface.specs.map_Empty_spec [variable, in DeBrLevel.Set.Setkit.SetOTwLInterface]
SetOTWithLeibnizInterface.specs.s [variable, in DeBrLevel.Set.Setkit.SetOTwLInterface]
SetOTWithLeibnizInterface.specs.singleton_notin_spec [variable, in DeBrLevel.Set.Setkit.SetOTwLInterface]
SetOTWithLeibnizInterface.specs.s' [variable, in DeBrLevel.Set.Setkit.SetOTwLInterface]
SetOTWithLeibnizInterface.specs.transpose_1 [variable, in DeBrLevel.Set.Setkit.SetOTwLInterface]
SetOTWithLeibnizInterface.specs.union_notin_spec [variable, in DeBrLevel.Set.Setkit.SetOTwLInterface]
SetOTWithLeibnizInterface.specs.union_add_spec [variable, in DeBrLevel.Set.Setkit.SetOTwLInterface]
SetOTWithLeibnizInterface.specs.x [variable, in DeBrLevel.Set.Setkit.SetOTwLInterface]
SetOTWithLeibnizInterface.specs.y [variable, in DeBrLevel.Set.Setkit.SetOTwLInterface]
SetOTWithLeibniz.add_shadow_leibniz [lemma, in DeBrLevel.Set.Setkit.SetOTwL]
SetOTWithLeibniz.add_notin_spec [lemma, in DeBrLevel.Set.Setkit.SetOTwL]
SetOTWithLeibniz.add_eq_leibniz [lemma, in DeBrLevel.Set.Setkit.SetOTwL]
SetOTWithLeibniz.Add_inv [lemma, in DeBrLevel.Set.Setkit.SetOTwL]
SetOTWithLeibniz.diff_notin_spec [lemma, in DeBrLevel.Set.Setkit.SetOTwL]
SetOTWithLeibniz.diff_notin_add_spec [lemma, in DeBrLevel.Set.Setkit.SetOTwL]
SetOTWithLeibniz.diff_in_add_spec [lemma, in DeBrLevel.Set.Setkit.SetOTwL]
SetOTWithLeibniz.eqb_refl [lemma, in DeBrLevel.Set.Setkit.SetOTwL]
SetOTWithLeibniz.gt_neq_nlt [lemma, in DeBrLevel.Set.Setkit.SetOTwL]
SetOTWithLeibniz.inter_notin_add_spec [lemma, in DeBrLevel.Set.Setkit.SetOTwL]
SetOTWithLeibniz.inter_in_add_spec [lemma, in DeBrLevel.Set.Setkit.SetOTwL]
SetOTWithLeibniz.ltb [definition, in DeBrLevel.Set.Setkit.SetOTwL]
SetOTWithLeibniz.ltb_lt [lemma, in DeBrLevel.Set.Setkit.SetOTwL]
SetOTWithLeibniz.map [definition, in DeBrLevel.Set.Setkit.SetOTwL]
SetOTWithLeibniz.map_union_spec [lemma, in DeBrLevel.Set.Setkit.SetOTwL]
SetOTWithLeibniz.map_add_in_spec [lemma, in DeBrLevel.Set.Setkit.SetOTwL]
SetOTWithLeibniz.map_add_notin_spec [lemma, in DeBrLevel.Set.Setkit.SetOTwL]
SetOTWithLeibniz.map_in_spec [lemma, in DeBrLevel.Set.Setkit.SetOTwL]
SetOTWithLeibniz.map_singleton_spec [lemma, in DeBrLevel.Set.Setkit.SetOTwL]
SetOTWithLeibniz.map_empty_spec [lemma, in DeBrLevel.Set.Setkit.SetOTwL]
SetOTWithLeibniz.map_Empty_spec [lemma, in DeBrLevel.Set.Setkit.SetOTwL]
SetOTWithLeibniz.proper_1 [instance, in DeBrLevel.Set.Setkit.SetOTwL]
SetOTWithLeibniz.props [section, in DeBrLevel.Set.Setkit.SetOTwL]
SetOTWithLeibniz.props.s [variable, in DeBrLevel.Set.Setkit.SetOTwL]
SetOTWithLeibniz.props.s' [variable, in DeBrLevel.Set.Setkit.SetOTwL]
SetOTWithLeibniz.props.x [variable, in DeBrLevel.Set.Setkit.SetOTwL]
SetOTWithLeibniz.props.y [variable, in DeBrLevel.Set.Setkit.SetOTwL]
SetOTWithLeibniz.singleton_notin_spec [lemma, in DeBrLevel.Set.Setkit.SetOTwL]
SetOTWithLeibniz.transpose_1 [lemma, in DeBrLevel.Set.Setkit.SetOTwL]
SetOTWithLeibniz.union_sym_leibniz [lemma, in DeBrLevel.Set.Setkit.SetOTwL]
SetOTWithLeibniz.union_notin_spec [lemma, in DeBrLevel.Set.Setkit.SetOTwL]
SetOTWithLeibniz.union_add_spec [lemma, in DeBrLevel.Set.Setkit.SetOTwL]
SetOTwL [library]
SetOTwLInterface [library]
Module Index
D
DecidableTypeWithLeibniz [in DeBrLevel.Core.LevelInterface]E
EqualityTypeWithLeibniz [in DeBrLevel.Core.LevelInterface]H
HasShift [in DeBrLevel.Core.LevelInterface]I
IsBdlLvl [in DeBrLevel.Core.LevelInterface]IsBdlLvlDT [in DeBrLevel.Core.LevelInterface]
IsBdlLvlDTWL [in DeBrLevel.Core.LevelInterface]
IsBdlLvlET [in DeBrLevel.Core.LevelInterface]
IsBdlLvlETWL [in DeBrLevel.Core.LevelInterface]
IsBdlLvlFullDT [in DeBrLevel.Core.LevelInterface]
IsBdlLvlFullDTWL [in DeBrLevel.Core.LevelInterface]
IsBdlLvlFullET [in DeBrLevel.Core.LevelInterface]
IsBdlLvlFullETWL [in DeBrLevel.Core.LevelInterface]
IsBdlLvlFullListETWL [in DeBrLevel.Datatype.ListLevel]
IsBdlLvlFullMapDInterface [in DeBrLevel.Map.MapLevelInterface]
IsBdlLvlFullMapKDInterface [in DeBrLevel.Map.MapLevelInterface]
IsBdlLvlFullMapKInterface [in DeBrLevel.Map.MapLevelInterface]
IsBdlLvlFullMapLVLDInterface [in DeBrLevel.Map.MapLevelInterface]
IsBdlLvlFullMapLVLInterface [in DeBrLevel.Map.MapLevelInterface]
IsBdlLvlFullOptET [in DeBrLevel.Datatype.OptionLevel]
IsBdlLvlFullOptETWL [in DeBrLevel.Datatype.OptionLevel]
IsBdlLvlFullOT [in DeBrLevel.Core.LevelInterface]
IsBdlLvlFullOTWL [in DeBrLevel.Core.LevelInterface]
IsBdlLvlFullPairET [in DeBrLevel.Datatype.PairLevel]
IsBdlLvlFullPairETWL [in DeBrLevel.Datatype.PairLevel]
IsBdlLvlFullPairOT [in DeBrLevel.Datatype.PairLevel]
IsBdlLvlFullPairOTWL [in DeBrLevel.Datatype.PairLevel]
IsBdlLvlFullSet [in DeBrLevel.Set.SetLevel]
IsBdlLvlFullSetInterface [in DeBrLevel.Set.SetLevelInterface]
IsBdlLvlListETWL [in DeBrLevel.Datatype.ListLevel]
IsBdlLvlMapD [in DeBrLevel.Map.MapLevelD]
IsBdlLvlMapDInterface [in DeBrLevel.Map.MapLevelInterface]
IsBdlLvlMapK [in DeBrLevel.Map.MapLevelK]
IsBdlLvlMapKD [in DeBrLevel.Map.MapLevelKD]
IsBdlLvlMapKDInterface [in DeBrLevel.Map.MapLevelInterface]
IsBdlLvlMapKInterface [in DeBrLevel.Map.MapLevelInterface]
IsBdlLvlMapLVL [in DeBrLevel.Map.MapLevelLvl]
IsBdlLvlMapLVLD [in DeBrLevel.Map.MapLevelLVLD]
IsBdlLvlMapLVLDInterface [in DeBrLevel.Map.MapLevelInterface]
IsBdlLvlMapLVLInterface [in DeBrLevel.Map.MapLevelInterface]
IsBdlLvlOptET [in DeBrLevel.Datatype.OptionLevel]
IsBdlLvlOptETWL [in DeBrLevel.Datatype.OptionLevel]
IsBdlLvlOT [in DeBrLevel.Core.LevelInterface]
IsBdlLvlOTWL [in DeBrLevel.Core.LevelInterface]
IsBdlLvlPairET [in DeBrLevel.Datatype.PairLevel]
IsBdlLvlPairETWL [in DeBrLevel.Datatype.PairLevel]
IsBdlLvlPairOT [in DeBrLevel.Datatype.PairLevel]
IsBdlLvlPairOTWL [in DeBrLevel.Datatype.PairLevel]
IsBdlLvlSet [in DeBrLevel.Set.SetLevel]
IsBdlLvlSetInterface [in DeBrLevel.Set.SetLevelInterface]
IsBindlessLeveled [in DeBrLevel.Core.LevelInterface]
IsBindlessLeveledDT [in DeBrLevel.Core.LevelInterface]
IsBindlessLeveledDTWithLeibniz [in DeBrLevel.Core.LevelInterface]
IsBindlessLeveledET [in DeBrLevel.Core.LevelInterface]
IsBindlessLeveledETWithLeibniz [in DeBrLevel.Core.LevelInterface]
IsBindlessLeveledEx [in DeBrLevel.Core.LevelInterface]
IsBindlessLeveledFullDT [in DeBrLevel.Core.LevelInterface]
IsBindlessLeveledFullDTWithLeibniz [in DeBrLevel.Core.LevelInterface]
IsBindlessLeveledFullET [in DeBrLevel.Core.LevelInterface]
IsBindlessLeveledFullETWithLeibniz [in DeBrLevel.Core.LevelInterface]
IsBindlessLeveledFullOT [in DeBrLevel.Core.LevelInterface]
IsBindlessLeveledFullOTWithLeibniz [in DeBrLevel.Core.LevelInterface]
IsBindlessLeveledOT [in DeBrLevel.Core.LevelInterface]
IsBindlessLeveledOTWithLeibniz [in DeBrLevel.Core.LevelInterface]
IsLeveled [in DeBrLevel.Core.LevelInterface]
IsLeveledDT [in DeBrLevel.Core.LevelInterface]
IsLeveledDTWithLeibniz [in DeBrLevel.Core.LevelInterface]
IsLeveledET [in DeBrLevel.Core.LevelInterface]
IsLeveledETWithLeibniz [in DeBrLevel.Core.LevelInterface]
IsLeveledFullDT [in DeBrLevel.Core.LevelInterface]
IsLeveledFullDTWithLeibniz [in DeBrLevel.Core.LevelInterface]
IsLeveledFullET [in DeBrLevel.Core.LevelInterface]
IsLeveledFullETWithLeibniz [in DeBrLevel.Core.LevelInterface]
IsLeveledFullOT [in DeBrLevel.Core.LevelInterface]
IsLeveledFullOTWithLeibniz [in DeBrLevel.Core.LevelInterface]
IsLeveledOT [in DeBrLevel.Core.LevelInterface]
IsLeveledOTWithLeibniz [in DeBrLevel.Core.LevelInterface]
IsLvl [in DeBrLevel.Core.LevelInterface]
IsLvlDT [in DeBrLevel.Core.LevelInterface]
IsLvlDTWL [in DeBrLevel.Core.LevelInterface]
IsLvlET [in DeBrLevel.Core.LevelInterface]
IsLvlETWL [in DeBrLevel.Core.LevelInterface]
IsLvlFullDT [in DeBrLevel.Core.LevelInterface]
IsLvlFullDTWL [in DeBrLevel.Core.LevelInterface]
IsLvlFullET [in DeBrLevel.Core.LevelInterface]
IsLvlFullETWL [in DeBrLevel.Core.LevelInterface]
IsLvlFullListETWL [in DeBrLevel.Datatype.ListLevel]
IsLvlFullMapDInterface [in DeBrLevel.Map.MapLevelInterface]
IsLvlFullMapKDInterface [in DeBrLevel.Map.MapLevelInterface]
IsLvlFullMapKInterface [in DeBrLevel.Map.MapLevelInterface]
IsLvlFullMapLVLDInterface [in DeBrLevel.Map.MapLevelInterface]
IsLvlFullMapLVLInterface [in DeBrLevel.Map.MapLevelInterface]
IsLvlFullOptET [in DeBrLevel.Datatype.OptionLevel]
IsLvlFullOptETWL [in DeBrLevel.Datatype.OptionLevel]
IsLvlFullOT [in DeBrLevel.Core.LevelInterface]
IsLvlFullOTWL [in DeBrLevel.Core.LevelInterface]
IsLvlFullPairET [in DeBrLevel.Datatype.PairLevel]
IsLvlFullPairETWL [in DeBrLevel.Datatype.PairLevel]
IsLvlFullPairOT [in DeBrLevel.Datatype.PairLevel]
IsLvlFullPairOTWL [in DeBrLevel.Datatype.PairLevel]
IsLvlFullSet [in DeBrLevel.Set.SetLevel]
IsLvlFullSetInterface [in DeBrLevel.Set.SetLevelInterface]
IsLvlListETWL [in DeBrLevel.Datatype.ListLevel]
IsLvlMapD [in DeBrLevel.Map.MapLevelD]
IsLvlMapDInterface [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapK [in DeBrLevel.Map.MapLevelK]
IsLvlMapKD [in DeBrLevel.Map.MapLevelKD]
IsLvlMapKDInterface [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKInterface [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVL [in DeBrLevel.Map.MapLevelLvl]
IsLvlMapLVLD [in DeBrLevel.Map.MapLevelLVLD]
IsLvlMapLVLDInterface [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLInterface [in DeBrLevel.Map.MapLevelInterface]
IsLvlOptET [in DeBrLevel.Datatype.OptionLevel]
IsLvlOptETWL [in DeBrLevel.Datatype.OptionLevel]
IsLvlOT [in DeBrLevel.Core.LevelInterface]
IsLvlOTWL [in DeBrLevel.Core.LevelInterface]
IsLvlPairET [in DeBrLevel.Datatype.PairLevel]
IsLvlPairETWL [in DeBrLevel.Datatype.PairLevel]
IsLvlPairOT [in DeBrLevel.Datatype.PairLevel]
IsLvlPairOTWL [in DeBrLevel.Datatype.PairLevel]
IsLvlSet [in DeBrLevel.Set.SetLevel]
IsLvlSetInterface [in DeBrLevel.Set.SetLevelInterface]
IsLvlSetLVLInterface [in DeBrLevel.Set.SetLevelInterface]
IsWF [in DeBrLevel.Core.LevelInterface]
IsWFb [in DeBrLevel.Core.LevelInterface]
IsWFFull [in DeBrLevel.Core.LevelInterface]
L
Level [in DeBrLevel.Core.Level]Levels [in DeBrLevel.Set.Levels]
Lvl [in DeBrLevel.Core.LevelInterface]
M
MakeBdlLvlFullSet [in DeBrLevel.Set.SetLevel]MakeBdlLvlFullSet.St [in DeBrLevel.Set.SetLevel]
MakeBdlLvlMapD [in DeBrLevel.Map.MapLevelD]
MakeBdlLvlMapD.Ext [in DeBrLevel.Map.MapLevelD]
MakeBdlLvlMapD.Raw [in DeBrLevel.Map.MapLevelD]
MakeBdlLvlMapK [in DeBrLevel.Map.MapLevelK]
MakeBdlLvlMapKD [in DeBrLevel.Map.MapLevelKD]
MakeBdlLvlMapKD.Ext [in DeBrLevel.Map.MapLevelKD]
MakeBdlLvlMapKD.Raw [in DeBrLevel.Map.MapLevelKD]
MakeBdlLvlMapK.Ext [in DeBrLevel.Map.MapLevelK]
MakeBdlLvlMapK.Raw [in DeBrLevel.Map.MapLevelK]
MakeBdlLvlMapLVL [in DeBrLevel.Map.MapLevelLvl]
MakeBdlLvlMapLVLD [in DeBrLevel.Map.MapLevelLVLD]
MakeBdlLvlMapLVLD.Ext [in DeBrLevel.Map.MapLevelLVLD]
MakeBdlLvlMapLVLD.Raw [in DeBrLevel.Map.MapLevelLVLD]
MakeBdlLvlMapLVL.Ext [in DeBrLevel.Map.MapLevelLvl]
MakeBdlLvlMapLVL.Raw [in DeBrLevel.Map.MapLevelLvl]
MakeBdlLvlSet [in DeBrLevel.Set.SetLevel]
MakeBdlLvlSet.St [in DeBrLevel.Set.SetLevel]
MakeLVL [in DeBrLevel.Set.Levels]
MakeLvlFullSet [in DeBrLevel.Set.SetLevel]
MakeLvlFullSet.St [in DeBrLevel.Set.SetLevel]
MakeLvlMapD [in DeBrLevel.Map.MapLevelD]
MakeLvlMapD.Ext [in DeBrLevel.Map.MapLevelD]
MakeLvlMapD.Raw [in DeBrLevel.Map.MapLevelD]
MakeLvlMapK [in DeBrLevel.Map.MapLevelK]
MakeLvlMapKD [in DeBrLevel.Map.MapLevelKD]
MakeLvlMapKD.Ext [in DeBrLevel.Map.MapLevelKD]
MakeLvlMapKD.Raw [in DeBrLevel.Map.MapLevelKD]
MakeLvlMapK.Ext [in DeBrLevel.Map.MapLevelK]
MakeLvlMapK.Raw [in DeBrLevel.Map.MapLevelK]
MakeLvlMapLVL [in DeBrLevel.Map.MapLevelLvl]
MakeLvlMapLVLD [in DeBrLevel.Map.MapLevelLVLD]
MakeLvlMapLVLD.Ext [in DeBrLevel.Map.MapLevelLVLD]
MakeLvlMapLVLD.Raw [in DeBrLevel.Map.MapLevelLVLD]
MakeLvlMapLVL.Ext [in DeBrLevel.Map.MapLevelLvl]
MakeLvlMapLVL.Raw [in DeBrLevel.Map.MapLevelLvl]
MakeLvlSet [in DeBrLevel.Set.SetLevel]
MakeLvlSet.St [in DeBrLevel.Set.SetLevel]
MakeLVL.St [in DeBrLevel.Set.Levels]
MapET [in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL [in DeBrLevel.Map.Mapkit.MapExt]
MapET.OP [in DeBrLevel.Map.Mapkit.MapExt]
MapInterface [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.OP [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface [in DeBrLevel.Map.Mapkit.MapExtInterface]
O
OrderedTypeWithLeibniz [in DeBrLevel.Core.LevelInterface]S
SetOTWithLeibniz [in DeBrLevel.Set.Setkit.SetOTwL]SetOTWithLeibnizInterface [in DeBrLevel.Set.Setkit.SetOTwLInterface]
Variable Index
H
HasShift.specs.k [in DeBrLevel.Core.LevelInterface]HasShift.specs.m [in DeBrLevel.Core.LevelInterface]
HasShift.specs.n [in DeBrLevel.Core.LevelInterface]
HasShift.specs.p [in DeBrLevel.Core.LevelInterface]
HasShift.specs.shift_eq_iff [in DeBrLevel.Core.LevelInterface]
HasShift.specs.shift_unfold_1 [in DeBrLevel.Core.LevelInterface]
HasShift.specs.shift_unfold [in DeBrLevel.Core.LevelInterface]
HasShift.specs.shift_permute [in DeBrLevel.Core.LevelInterface]
HasShift.specs.shift_trans [in DeBrLevel.Core.LevelInterface]
HasShift.specs.shift_zero_refl [in DeBrLevel.Core.LevelInterface]
HasShift.specs.t [in DeBrLevel.Core.LevelInterface]
HasShift.specs.t' [in DeBrLevel.Core.LevelInterface]
I
IsLeveled.specs.k [in DeBrLevel.Core.LevelInterface]IsLeveled.specs.m [in DeBrLevel.Core.LevelInterface]
IsLeveled.specs.n [in DeBrLevel.Core.LevelInterface]
IsLeveled.specs.p [in DeBrLevel.Core.LevelInterface]
IsLeveled.specs.shift_preserves_wf_zero [in DeBrLevel.Core.LevelInterface]
IsLeveled.specs.shift_preserves_wf_2 [in DeBrLevel.Core.LevelInterface]
IsLeveled.specs.shift_preserves_wf_1 [in DeBrLevel.Core.LevelInterface]
IsLeveled.specs.shift_preserves_wf [in DeBrLevel.Core.LevelInterface]
IsLeveled.specs.shift_preserves_wf_gen [in DeBrLevel.Core.LevelInterface]
IsLeveled.specs.t [in DeBrLevel.Core.LevelInterface]
IsLvlFullListETWL.props.k [in DeBrLevel.Datatype.ListLevel]
IsLvlFullListETWL.props.t [in DeBrLevel.Datatype.ListLevel]
IsLvlFullOptET.valid.n [in DeBrLevel.Datatype.OptionLevel]
IsLvlFullOptET.valid.t [in DeBrLevel.Datatype.OptionLevel]
IsLvlFullPairET.is_wf.t [in DeBrLevel.Datatype.PairLevel]
IsLvlFullPairET.is_wf.n [in DeBrLevel.Datatype.PairLevel]
IsLvlFullPairOT.is_wf.t [in DeBrLevel.Datatype.PairLevel]
IsLvlFullPairOT.is_wf.n [in DeBrLevel.Datatype.PairLevel]
IsLvlListETWL.shift_props.t' [in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.shift_props.t [in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.shift_props.k'' [in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.shift_props.k' [in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.shift_props.k [in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.shift_props.lb [in DeBrLevel.Datatype.ListLevel]
IsLvlMapDInterface.specs.k [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapDInterface.specs.m [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapDInterface.specs.m' [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapDInterface.specs.n [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapDInterface.specs.p [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapDInterface.specs.shift_find_iff [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapDInterface.specs.shift_notin_iff [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapDInterface.specs.shift_in_iff [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapDInterface.specs.shift_remove [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapDInterface.specs.shift_Add_iff [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapDInterface.specs.shift_Add [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapDInterface.specs.shift_add [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapDInterface.specs.shift_Empty [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapDInterface.specs.shift_Empty_iff [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapDInterface.specs.v [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapDInterface.specs.Wf_update [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapDInterface.specs.Wf_find [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapDInterface.specs.Wf_add [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapDInterface.specs.Wf_add_in [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapDInterface.specs.Wf_Add [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapDInterface.specs.Wf_Add_iff [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapDInterface.specs.Wf_empty [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapDInterface.specs.Wf_Empty [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapDInterface.specs.x [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKDInterface.specs.k [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKDInterface.specs.m [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKDInterface.specs.m' [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKDInterface.specs.n [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKDInterface.specs.p [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKDInterface.specs.shift_find_e_1 [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKDInterface.specs.shift_find_e [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKDInterface.specs.shift_find_iff [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKDInterface.specs.shift_notin_iff [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKDInterface.specs.shift_in_iff [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKDInterface.specs.shift_in_e [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKDInterface.specs.shift_remove [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKDInterface.specs.shift_Add_iff [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKDInterface.specs.shift_Add [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKDInterface.specs.shift_add [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKDInterface.specs.shift_Empty [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKDInterface.specs.shift_Empty_iff [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKDInterface.specs.v [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKDInterface.specs.Wf_update [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKDInterface.specs.Wf_in [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKDInterface.specs.Wf_find [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKDInterface.specs.Wf_Add [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKDInterface.specs.Wf_Add_iff [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKDInterface.specs.Wf_add_in [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKDInterface.specs.Wf_add_notin [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKDInterface.specs.Wf_add [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKDInterface.specs.Wf_empty [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKDInterface.specs.Wf_Empty_iff [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKDInterface.specs.Wf_Empty [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKDInterface.specs.x [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKInterface.specs.k [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKInterface.specs.m [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKInterface.specs.m' [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKInterface.specs.n [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKInterface.specs.p [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKInterface.specs.shift_find [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKInterface.specs.shift_notin_iff [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKInterface.specs.shift_in_iff [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKInterface.specs.shift_in_e [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKInterface.specs.shift_remove [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKInterface.specs.shift_Add_iff [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKInterface.specs.shift_Add [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKInterface.specs.shift_add [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKInterface.specs.shift_Empty [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKInterface.specs.shift_Empty_iff [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKInterface.specs.v [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKInterface.specs.Wf_in [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKInterface.specs.Wf_Add_iff [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKInterface.specs.Wf_add_in [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKInterface.specs.Wf_add_iff [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKInterface.specs.Wf_empty [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKInterface.specs.Wf_Empty_iff [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKInterface.specs.Wf_Empty [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKInterface.specs.x [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLDInterface.props.k [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLDInterface.props.m [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLDInterface.props.n [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLDInterface.props.shift_new_key_le [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLDInterface.props.shift_max_key_le [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLDInterface.props.shift_max_key_gt_iff [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLDInterface.props.shift_max_refl [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLDInterface.props.shift_new_refl [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLDInterface.props.shift_new_notin [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLDInterface.props.shift_in_new_key [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLDInterface.props.shift_find_Wf [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLDInterface.props.t [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLDInterface.props.t' [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLDInterface.props.Wf_in_iff [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLDInterface.props.x [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLInterface.specs.k [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLInterface.specs.m [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLInterface.specs.n [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLInterface.specs.shift_new_key_le [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLInterface.specs.shift_max_key_le [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLInterface.specs.shift_max_key_gt_iff [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLInterface.specs.shift_max_refl [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLInterface.specs.shift_new_refl [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLInterface.specs.shift_new_notin [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLInterface.specs.shift_find_Wf [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLInterface.specs.shift_in_new_key [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLInterface.specs.t [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLInterface.specs.t' [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLInterface.specs.Wf_in_iff [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLInterface.specs.x [in DeBrLevel.Map.MapLevelInterface]
IsLvlOptET.shift.k [in DeBrLevel.Datatype.OptionLevel]
IsLvlOptET.shift.m [in DeBrLevel.Datatype.OptionLevel]
IsLvlOptET.shift.n [in DeBrLevel.Datatype.OptionLevel]
IsLvlOptET.shift.p [in DeBrLevel.Datatype.OptionLevel]
IsLvlOptET.shift.t [in DeBrLevel.Datatype.OptionLevel]
IsLvlOptET.shift.t1 [in DeBrLevel.Datatype.OptionLevel]
IsLvlPairET.shift.k [in DeBrLevel.Datatype.PairLevel]
IsLvlPairET.shift.m [in DeBrLevel.Datatype.PairLevel]
IsLvlPairET.shift.n [in DeBrLevel.Datatype.PairLevel]
IsLvlPairET.shift.p [in DeBrLevel.Datatype.PairLevel]
IsLvlPairET.shift.t [in DeBrLevel.Datatype.PairLevel]
IsLvlPairOT.shift.k [in DeBrLevel.Datatype.PairLevel]
IsLvlPairOT.shift.m [in DeBrLevel.Datatype.PairLevel]
IsLvlPairOT.shift.n [in DeBrLevel.Datatype.PairLevel]
IsLvlPairOT.shift.p [in DeBrLevel.Datatype.PairLevel]
IsLvlPairOT.shift.t [in DeBrLevel.Datatype.PairLevel]
IsLvlPairOT.shift.t1 [in DeBrLevel.Datatype.PairLevel]
IsLvlSetInterface.specs.m [in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.specs.n [in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.specs.shift_notin_iff [in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.specs.shift_in_e [in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.specs.shift_in_iff [in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.specs.shift_remove [in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.specs.shift_add [in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.specs.shift_add_in [in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.specs.shift_add_notin [in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.specs.shift_diff [in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.specs.shift_inter [in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.specs.shift_union [in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.specs.shift_singleton [in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.specs.shift_empty [in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.specs.shift_Empty [in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.specs.t [in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.specs.t' [in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.specs.v [in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.specs.Wf_in [in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.specs.Wf_singleton_iff [in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.specs.Wf_union_iff [in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.specs.Wf_empty [in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.specs.Wf_add_iff [in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.specs.Wf_unfold [in DeBrLevel.Set.SetLevelInterface]
IsLvlSetLVLInterface.specifications.k [in DeBrLevel.Set.SetLevelInterface]
IsLvlSetLVLInterface.specifications.m [in DeBrLevel.Set.SetLevelInterface]
IsLvlSetLVLInterface.specifications.max_key_add_max [in DeBrLevel.Set.SetLevelInterface]
IsLvlSetLVLInterface.specifications.max_key_Add_max [in DeBrLevel.Set.SetLevelInterface]
IsLvlSetLVLInterface.specifications.max_key_empty [in DeBrLevel.Set.SetLevelInterface]
IsLvlSetLVLInterface.specifications.max_key_Empty [in DeBrLevel.Set.SetLevelInterface]
IsLvlSetLVLInterface.specifications.n [in DeBrLevel.Set.SetLevelInterface]
IsLvlSetLVLInterface.specifications.new_key_in [in DeBrLevel.Set.SetLevelInterface]
IsLvlSetLVLInterface.specifications.new_key_add_max [in DeBrLevel.Set.SetLevelInterface]
IsLvlSetLVLInterface.specifications.new_key_Add_max [in DeBrLevel.Set.SetLevelInterface]
IsLvlSetLVLInterface.specifications.new_key_empty [in DeBrLevel.Set.SetLevelInterface]
IsLvlSetLVLInterface.specifications.new_key_Empty [in DeBrLevel.Set.SetLevelInterface]
IsLvlSetLVLInterface.specifications.p [in DeBrLevel.Set.SetLevelInterface]
IsLvlSetLVLInterface.specifications.s [in DeBrLevel.Set.SetLevelInterface]
IsLvlSetLVLInterface.specifications.shift_new_refl [in DeBrLevel.Set.SetLevelInterface]
IsLvlSetLVLInterface.specifications.shift_permute_2 [in DeBrLevel.Set.SetLevelInterface]
IsLvlSetLVLInterface.specifications.shift_permute_1 [in DeBrLevel.Set.SetLevelInterface]
IsLvlSetLVLInterface.specifications.s' [in DeBrLevel.Set.SetLevelInterface]
IsLvlSetLVLInterface.specifications.v [in DeBrLevel.Set.SetLevelInterface]
IsLvlSet.specs.k [in DeBrLevel.Set.SetLevel]
IsLvlSet.specs.m [in DeBrLevel.Set.SetLevel]
IsLvlSet.specs.n [in DeBrLevel.Set.SetLevel]
IsLvlSet.specs.s [in DeBrLevel.Set.SetLevel]
IsLvlSet.specs.s' [in DeBrLevel.Set.SetLevel]
IsLvlSet.specs.v [in DeBrLevel.Set.SetLevel]
IsWFFull.specs.k [in DeBrLevel.Core.LevelInterface]
IsWFFull.specs.notWf_is_wf_false [in DeBrLevel.Core.LevelInterface]
IsWFFull.specs.t [in DeBrLevel.Core.LevelInterface]
IsWFFull.specs.Wf_is_wf_true [in DeBrLevel.Core.LevelInterface]
L
Level.lt_eq.t2 [in DeBrLevel.Core.Level]Level.lt_eq.t1 [in DeBrLevel.Core.Level]
Level.shift.k [in DeBrLevel.Core.Level]
Level.shift.m [in DeBrLevel.Core.Level]
Level.shift.n [in DeBrLevel.Core.Level]
Level.shift.p [in DeBrLevel.Core.Level]
Level.shift.t [in DeBrLevel.Core.Level]
Level.shift.t1 [in DeBrLevel.Core.Level]
M
MapInterface.specifications.add_remove [in DeBrLevel.Map.Mapkit.MapExtInterface]MapInterface.specifications.add_shadow [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.specifications.e [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.specifications.Empty_eq [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.specifications.e' [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.specifications.For_all_add_notin [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.specifications.For_all_add [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.specifications.For_all_Empty [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.specifications.For_all_empty [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.specifications.is_empty_add [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.specifications.is_empty_Add [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.specifications.m [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.specifications.m' [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.specifications.m1 [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.specifications.notEmpty_find [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.specifications.notEmpty_Add [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.specifications.P [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.specifications.Submap_find [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.specifications.Submap_notin [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.specifications.Submap_in [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.specifications.Submap_add_1 [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.specifications.Submap_add_2 [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.specifications.Submap_add [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.specifications.Submap_Add_1 [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.specifications.Submap_Add_find [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.specifications.Submap_Add_in [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.specifications.Submap_Add [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.specifications.Submap_empty_bot [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.specifications.Submap_Empty [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.specifications.Submap_Empty_bot [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.specifications.x [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.m [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.max_key_Submap [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.max_key_in [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.max_key_notin [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.max_key_add_max [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.max_key_add_max_key [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.max_key_add_iff [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.max_key_add_in [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.max_key_add_r [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.max_key_add_l [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.max_key_Add_max [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.max_key_Add_r [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.max_key_Add_l [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.max_key_empty [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.max_key_Empty [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.max_key_ub [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.m' [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.new_key_Submap_add [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.new_key_Submap [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.new_key_in [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.new_key_notin [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.new_key_add_new_key [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.new_key_add_in [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.new_key_add_r [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.new_key_add_l [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.new_key_add_max [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.new_key_Add_max [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.new_key_Add_r [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.new_key_Add_l [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.new_key_empty [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.new_key_Empty [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.new_key_unfold [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.new_key_geq_max_key [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.v [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.v' [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.specs.x [in DeBrLevel.Map.Mapkit.MapExtInterface]
S
SetOTWithLeibnizInterface.specs.add_notin_spec [in DeBrLevel.Set.Setkit.SetOTwLInterface]SetOTWithLeibnizInterface.specs.add_eq_leibniz [in DeBrLevel.Set.Setkit.SetOTwLInterface]
SetOTWithLeibnizInterface.specs.Add_inv [in DeBrLevel.Set.Setkit.SetOTwLInterface]
SetOTWithLeibnizInterface.specs.diff_notin_spec [in DeBrLevel.Set.Setkit.SetOTwLInterface]
SetOTWithLeibnizInterface.specs.diff_notin_add_spec [in DeBrLevel.Set.Setkit.SetOTwLInterface]
SetOTWithLeibnizInterface.specs.diff_in_add_spec [in DeBrLevel.Set.Setkit.SetOTwLInterface]
SetOTWithLeibnizInterface.specs.eqb_refl [in DeBrLevel.Set.Setkit.SetOTwLInterface]
SetOTWithLeibnizInterface.specs.f [in DeBrLevel.Set.Setkit.SetOTwLInterface]
SetOTWithLeibnizInterface.specs.gt_neq_nlt [in DeBrLevel.Set.Setkit.SetOTwLInterface]
SetOTWithLeibnizInterface.specs.inter_notin_add_spec [in DeBrLevel.Set.Setkit.SetOTwLInterface]
SetOTWithLeibnizInterface.specs.inter_in_add_spec [in DeBrLevel.Set.Setkit.SetOTwLInterface]
SetOTWithLeibnizInterface.specs.ltb_lt [in DeBrLevel.Set.Setkit.SetOTwLInterface]
SetOTWithLeibnizInterface.specs.map_union_spec [in DeBrLevel.Set.Setkit.SetOTwLInterface]
SetOTWithLeibnizInterface.specs.map_add_in_spec [in DeBrLevel.Set.Setkit.SetOTwLInterface]
SetOTWithLeibnizInterface.specs.map_add_notin_spec [in DeBrLevel.Set.Setkit.SetOTwLInterface]
SetOTWithLeibnizInterface.specs.map_in_spec [in DeBrLevel.Set.Setkit.SetOTwLInterface]
SetOTWithLeibnizInterface.specs.map_singleton_spec [in DeBrLevel.Set.Setkit.SetOTwLInterface]
SetOTWithLeibnizInterface.specs.map_empty_spec [in DeBrLevel.Set.Setkit.SetOTwLInterface]
SetOTWithLeibnizInterface.specs.map_Empty_spec [in DeBrLevel.Set.Setkit.SetOTwLInterface]
SetOTWithLeibnizInterface.specs.s [in DeBrLevel.Set.Setkit.SetOTwLInterface]
SetOTWithLeibnizInterface.specs.singleton_notin_spec [in DeBrLevel.Set.Setkit.SetOTwLInterface]
SetOTWithLeibnizInterface.specs.s' [in DeBrLevel.Set.Setkit.SetOTwLInterface]
SetOTWithLeibnizInterface.specs.transpose_1 [in DeBrLevel.Set.Setkit.SetOTwLInterface]
SetOTWithLeibnizInterface.specs.union_notin_spec [in DeBrLevel.Set.Setkit.SetOTwLInterface]
SetOTWithLeibnizInterface.specs.union_add_spec [in DeBrLevel.Set.Setkit.SetOTwLInterface]
SetOTWithLeibnizInterface.specs.x [in DeBrLevel.Set.Setkit.SetOTwLInterface]
SetOTWithLeibnizInterface.specs.y [in DeBrLevel.Set.Setkit.SetOTwLInterface]
SetOTWithLeibniz.props.s [in DeBrLevel.Set.Setkit.SetOTwL]
SetOTWithLeibniz.props.s' [in DeBrLevel.Set.Setkit.SetOTwL]
SetOTWithLeibniz.props.x [in DeBrLevel.Set.Setkit.SetOTwL]
SetOTWithLeibniz.props.y [in DeBrLevel.Set.Setkit.SetOTwL]
Library Index
L
LevelLevelInterface
Levels
ListLevel
M
MapExtMapExtInterface
MapLevelD
MapLevelInterface
MapLevelK
MapLevelKD
MapLevelLvl
MapLevelLVLD
O
OptionLevelP
PairLevelS
SetLevelSetLevelInterface
SetOTwL
SetOTwLInterface
Lemma Index
I
IsBdlLvlFullListETWL.shift_wf_refl [in DeBrLevel.Datatype.ListLevel]IsBdlLvlFullOptETWL.eq_leibniz [in DeBrLevel.Datatype.OptionLevel]
IsBdlLvlFullOptET.shift_wf_refl [in DeBrLevel.Datatype.OptionLevel]
IsBdlLvlFullPairETWL.eq_leibniz [in DeBrLevel.Datatype.PairLevel]
IsBdlLvlFullPairET.shift_wf_refl [in DeBrLevel.Datatype.PairLevel]
IsBdlLvlFullPairOTWL.eq_leibniz [in DeBrLevel.Datatype.PairLevel]
IsBdlLvlFullPairOT.shift_wf_refl [in DeBrLevel.Datatype.PairLevel]
IsBdlLvlFullSet.shift_wf_refl [in DeBrLevel.Set.SetLevel]
IsBdlLvlFullSet.Wf_in_iff [in DeBrLevel.Set.SetLevel]
IsBdlLvlListETWL.shift_wf_refl [in DeBrLevel.Datatype.ListLevel]
IsBdlLvlMapD.shift_wf_refl [in DeBrLevel.Map.MapLevelD]
IsBdlLvlMapKD.shift_find_Wf [in DeBrLevel.Map.MapLevelKD]
IsBdlLvlMapKD.shift_wf_refl [in DeBrLevel.Map.MapLevelKD]
IsBdlLvlMapKD.Wf_in_iff [in DeBrLevel.Map.MapLevelKD]
IsBdlLvlMapK.shift_find_Wf [in DeBrLevel.Map.MapLevelK]
IsBdlLvlMapK.shift_wf_refl [in DeBrLevel.Map.MapLevelK]
IsBdlLvlMapK.Wf_in_iff [in DeBrLevel.Map.MapLevelK]
IsBdlLvlMapLVLD.shift_wf_refl [in DeBrLevel.Map.MapLevelLVLD]
IsBdlLvlMapLVL.shift_wf_refl [in DeBrLevel.Map.MapLevelLvl]
IsBdlLvlOptETWL.eq_leibniz [in DeBrLevel.Datatype.OptionLevel]
IsBdlLvlOptET.shift_wf_refl [in DeBrLevel.Datatype.OptionLevel]
IsBdlLvlPairETWL.eq_leibniz [in DeBrLevel.Datatype.PairLevel]
IsBdlLvlPairET.shift_wf_refl [in DeBrLevel.Datatype.PairLevel]
IsBdlLvlPairOTWL.eq_leibniz [in DeBrLevel.Datatype.PairLevel]
IsBdlLvlPairOT.shift_wf_refl [in DeBrLevel.Datatype.PairLevel]
IsBdlLvlSet.shift_wf_refl [in DeBrLevel.Set.SetLevel]
IsBdlLvlSet.Wf_in_iff [in DeBrLevel.Set.SetLevel]
IsLvlFullListETWL.is_wf_eq [in DeBrLevel.Datatype.ListLevel]
IsLvlFullListETWL.notWf_is_wf_false [in DeBrLevel.Datatype.ListLevel]
IsLvlFullListETWL.Wf_is_wf_true [in DeBrLevel.Datatype.ListLevel]
IsLvlFullOptETWL.eq_leibniz [in DeBrLevel.Datatype.OptionLevel]
IsLvlFullOptET.notWf_is_wf_false [in DeBrLevel.Datatype.OptionLevel]
IsLvlFullOptET.Wf_is_wf_true [in DeBrLevel.Datatype.OptionLevel]
IsLvlFullPairETWL.eq_leibniz [in DeBrLevel.Datatype.PairLevel]
IsLvlFullPairET.notWf_is_wf_false [in DeBrLevel.Datatype.PairLevel]
IsLvlFullPairET.Wf_is_wf_true [in DeBrLevel.Datatype.PairLevel]
IsLvlFullPairOTWL.eq_leibniz [in DeBrLevel.Datatype.PairLevel]
IsLvlFullPairOT.is_wf_eq [in DeBrLevel.Datatype.PairLevel]
IsLvlFullPairOT.notWf_is_wf_false [in DeBrLevel.Datatype.PairLevel]
IsLvlFullPairOT.Wf_is_wf_true [in DeBrLevel.Datatype.PairLevel]
IsLvlFullSet.notWf_is_wf_false [in DeBrLevel.Set.SetLevel]
IsLvlFullSet.Wf_is_wf_true [in DeBrLevel.Set.SetLevel]
IsLvlListETWL.eq_leibniz [in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.shift_preserves_wf_zero [in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.shift_preserves_wf_2 [in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.shift_preserves_wf_gen [in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.shift_preserves_wf_1 [in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.shift_preserves_wf [in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.shift_notin [in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.shift_in_e [in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.shift_in [in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.shift_app [in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.shift_cons [in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.shift_nil [in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.shift_unfold_1 [in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.shift_unfold [in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.shift_permute [in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.shift_trans [in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.shift_zero_refl [in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.shift_eq_iff [in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.Wf_weakening [in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.Wf_in [in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.Wf_app [in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.Wf_cons [in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.Wf_nil [in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.Wf_unfold [in DeBrLevel.Datatype.ListLevel]
IsLvlMapD.shift_preserves_wf_zero [in DeBrLevel.Map.MapLevelD]
IsLvlMapD.shift_preserves_wf [in DeBrLevel.Map.MapLevelD]
IsLvlMapD.shift_preserves_wf_2 [in DeBrLevel.Map.MapLevelD]
IsLvlMapD.shift_preserves_wf_gen [in DeBrLevel.Map.MapLevelD]
IsLvlMapD.shift_preserves_wf_1 [in DeBrLevel.Map.MapLevelD]
IsLvlMapD.shift_unfold_1 [in DeBrLevel.Map.MapLevelD]
IsLvlMapD.shift_unfold [in DeBrLevel.Map.MapLevelD]
IsLvlMapD.shift_permute [in DeBrLevel.Map.MapLevelD]
IsLvlMapD.shift_trans [in DeBrLevel.Map.MapLevelD]
IsLvlMapD.shift_zero_refl [in DeBrLevel.Map.MapLevelD]
IsLvlMapD.shift_remove [in DeBrLevel.Map.MapLevelD]
IsLvlMapD.shift_Add_iff [in DeBrLevel.Map.MapLevelD]
IsLvlMapD.shift_eq_iff [in DeBrLevel.Map.MapLevelD]
IsLvlMapD.shift_Empty_iff [in DeBrLevel.Map.MapLevelD]
IsLvlMapD.shift_find_iff [in DeBrLevel.Map.MapLevelD]
IsLvlMapD.shift_notin_iff [in DeBrLevel.Map.MapLevelD]
IsLvlMapD.shift_in_iff [in DeBrLevel.Map.MapLevelD]
IsLvlMapD.shift_in_2 [in DeBrLevel.Map.MapLevelD]
IsLvlMapD.shift_in_1 [in DeBrLevel.Map.MapLevelD]
IsLvlMapD.shift_Add [in DeBrLevel.Map.MapLevelD]
IsLvlMapD.shift_add [in DeBrLevel.Map.MapLevelD]
IsLvlMapD.shift_add_notin [in DeBrLevel.Map.MapLevelD]
IsLvlMapD.shift_Empty [in DeBrLevel.Map.MapLevelD]
IsLvlMapD.shift_diamond [in DeBrLevel.Map.MapLevelD]
IsLvlMapD.Wf_weakening [in DeBrLevel.Map.MapLevelD]
IsLvlMapD.Wf_update [in DeBrLevel.Map.MapLevelD]
IsLvlMapD.Wf_find [in DeBrLevel.Map.MapLevelD]
IsLvlMapD.Wf_Add [in DeBrLevel.Map.MapLevelD]
IsLvlMapD.Wf_add [in DeBrLevel.Map.MapLevelD]
IsLvlMapD.Wf_add_in [in DeBrLevel.Map.MapLevelD]
IsLvlMapD.Wf_add_notin [in DeBrLevel.Map.MapLevelD]
IsLvlMapD.Wf_Add_iff [in DeBrLevel.Map.MapLevelD]
IsLvlMapD.Wf_empty [in DeBrLevel.Map.MapLevelD]
IsLvlMapD.Wf_Empty_iff [in DeBrLevel.Map.MapLevelD]
IsLvlMapD.Wf_Empty [in DeBrLevel.Map.MapLevelD]
IsLvlMapD.Wf_func_diamond [in DeBrLevel.Map.MapLevelD]
IsLvlMapKD.shift_preserves_wf_zero [in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_preserves_wf [in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_preserves_wf_2 [in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_preserves_wf_gen [in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_preserves_wf_1 [in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_unfold_1 [in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_unfold [in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_permute [in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_trans [in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_zero_refl [in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_remove [in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_Add_iff [in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_find_e_1 [in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_in_e [in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_eq_iff [in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_find_e [in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_find_iff [in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_find_2 [in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_find_1 [in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_notin_iff [in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_in_iff [in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_in_2 [in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_in_1 [in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_Add [in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_add [in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_Add_2 [in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_add_notin [in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_Empty_iff [in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_Add_1 [in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_Empty [in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_diamond [in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.Wf_weakening [in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.Wf_update [in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.Wf_Add [in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.Wf_add_in [in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.Wf_in [in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.Wf_find [in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.Wf_add [in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.Wf_Add_iff [in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.Wf_add_notin [in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.Wf_empty [in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.Wf_Empty_iff [in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.Wf_Empty [in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.Wf_func_diamond [in DeBrLevel.Map.MapLevelKD]
IsLvlMapK.shift_preserves_wf_zero [in DeBrLevel.Map.MapLevelK]
IsLvlMapK.shift_preserves_wf [in DeBrLevel.Map.MapLevelK]
IsLvlMapK.shift_preserves_wf_2 [in DeBrLevel.Map.MapLevelK]
IsLvlMapK.shift_preserves_wf_gen [in DeBrLevel.Map.MapLevelK]
IsLvlMapK.shift_preserves_wf_1 [in DeBrLevel.Map.MapLevelK]
IsLvlMapK.shift_unfold_1 [in DeBrLevel.Map.MapLevelK]
IsLvlMapK.shift_unfold [in DeBrLevel.Map.MapLevelK]
IsLvlMapK.shift_permute [in DeBrLevel.Map.MapLevelK]
IsLvlMapK.shift_trans [in DeBrLevel.Map.MapLevelK]
IsLvlMapK.shift_zero_refl [in DeBrLevel.Map.MapLevelK]
IsLvlMapK.shift_remove [in DeBrLevel.Map.MapLevelK]
IsLvlMapK.shift_Add_iff [in DeBrLevel.Map.MapLevelK]
IsLvlMapK.shift_eq_iff [in DeBrLevel.Map.MapLevelK]
IsLvlMapK.shift_in_e [in DeBrLevel.Map.MapLevelK]
IsLvlMapK.shift_notin_iff [in DeBrLevel.Map.MapLevelK]
IsLvlMapK.shift_in_iff [in DeBrLevel.Map.MapLevelK]
IsLvlMapK.shift_in_2 [in DeBrLevel.Map.MapLevelK]
IsLvlMapK.shift_in_1 [in DeBrLevel.Map.MapLevelK]
IsLvlMapK.shift_find [in DeBrLevel.Map.MapLevelK]
IsLvlMapK.shift_Add [in DeBrLevel.Map.MapLevelK]
IsLvlMapK.shift_add [in DeBrLevel.Map.MapLevelK]
IsLvlMapK.shift_add_notin [in DeBrLevel.Map.MapLevelK]
IsLvlMapK.shift_Add_2 [in DeBrLevel.Map.MapLevelK]
IsLvlMapK.shift_Add_1 [in DeBrLevel.Map.MapLevelK]
IsLvlMapK.shift_Empty_iff [in DeBrLevel.Map.MapLevelK]
IsLvlMapK.shift_Empty [in DeBrLevel.Map.MapLevelK]
IsLvlMapK.shift_diamond [in DeBrLevel.Map.MapLevelK]
IsLvlMapK.Wf_weakening [in DeBrLevel.Map.MapLevelK]
IsLvlMapK.Wf_in [in DeBrLevel.Map.MapLevelK]
IsLvlMapK.Wf_Add_iff [in DeBrLevel.Map.MapLevelK]
IsLvlMapK.Wf_add_iff [in DeBrLevel.Map.MapLevelK]
IsLvlMapK.Wf_add_in [in DeBrLevel.Map.MapLevelK]
IsLvlMapK.Wf_add_notin [in DeBrLevel.Map.MapLevelK]
IsLvlMapK.Wf_Add [in DeBrLevel.Map.MapLevelK]
IsLvlMapK.Wf_empty [in DeBrLevel.Map.MapLevelK]
IsLvlMapK.Wf_Empty_iff [in DeBrLevel.Map.MapLevelK]
IsLvlMapK.Wf_Empty [in DeBrLevel.Map.MapLevelK]
IsLvlMapK.Wf_func_diamond [in DeBrLevel.Map.MapLevelK]
IsLvlMapLVLD.shift_in_new_key [in DeBrLevel.Map.MapLevelLVLD]
IsLvlMapLVLD.shift_find_Wf [in DeBrLevel.Map.MapLevelLVLD]
IsLvlMapLVLD.shift_new_key_le [in DeBrLevel.Map.MapLevelLVLD]
IsLvlMapLVLD.shift_max_key_le [in DeBrLevel.Map.MapLevelLVLD]
IsLvlMapLVLD.shift_max_key_gt_iff [in DeBrLevel.Map.MapLevelLVLD]
IsLvlMapLVLD.shift_new_refl [in DeBrLevel.Map.MapLevelLVLD]
IsLvlMapLVLD.shift_max_refl [in DeBrLevel.Map.MapLevelLVLD]
IsLvlMapLVLD.shift_new_notin [in DeBrLevel.Map.MapLevelLVLD]
IsLvlMapLVLD.Wf_in_iff [in DeBrLevel.Map.MapLevelLVLD]
IsLvlMapLVL.shift_in_new_key [in DeBrLevel.Map.MapLevelLvl]
IsLvlMapLVL.shift_find_Wf [in DeBrLevel.Map.MapLevelLvl]
IsLvlMapLVL.shift_new_key_le [in DeBrLevel.Map.MapLevelLvl]
IsLvlMapLVL.shift_max_key_le [in DeBrLevel.Map.MapLevelLvl]
IsLvlMapLVL.shift_max_key_gt_iff [in DeBrLevel.Map.MapLevelLvl]
IsLvlMapLVL.shift_new_refl [in DeBrLevel.Map.MapLevelLvl]
IsLvlMapLVL.shift_max_refl [in DeBrLevel.Map.MapLevelLvl]
IsLvlMapLVL.shift_new_notin [in DeBrLevel.Map.MapLevelLvl]
IsLvlMapLVL.Wf_in_iff [in DeBrLevel.Map.MapLevelLvl]
IsLvlOptETWL.eq_leibniz [in DeBrLevel.Datatype.OptionLevel]
IsLvlOptET.shift_preserves_wf_zero [in DeBrLevel.Datatype.OptionLevel]
IsLvlOptET.shift_preserves_wf_2 [in DeBrLevel.Datatype.OptionLevel]
IsLvlOptET.shift_preserves_wf_gen [in DeBrLevel.Datatype.OptionLevel]
IsLvlOptET.shift_preserves_wf_1 [in DeBrLevel.Datatype.OptionLevel]
IsLvlOptET.shift_preserves_wf [in DeBrLevel.Datatype.OptionLevel]
IsLvlOptET.shift_unfold_1 [in DeBrLevel.Datatype.OptionLevel]
IsLvlOptET.shift_unfold [in DeBrLevel.Datatype.OptionLevel]
IsLvlOptET.shift_permute [in DeBrLevel.Datatype.OptionLevel]
IsLvlOptET.shift_trans [in DeBrLevel.Datatype.OptionLevel]
IsLvlOptET.shift_zero_refl [in DeBrLevel.Datatype.OptionLevel]
IsLvlOptET.shift_eq_iff [in DeBrLevel.Datatype.OptionLevel]
IsLvlOptET.Wf_weakening [in DeBrLevel.Datatype.OptionLevel]
IsLvlPairETWL.eq_leibniz [in DeBrLevel.Datatype.PairLevel]
IsLvlPairET.shift_preserves_wf_zero [in DeBrLevel.Datatype.PairLevel]
IsLvlPairET.shift_preserves_wf_2 [in DeBrLevel.Datatype.PairLevel]
IsLvlPairET.shift_preserves_wf_gen [in DeBrLevel.Datatype.PairLevel]
IsLvlPairET.shift_preserves_wf_1 [in DeBrLevel.Datatype.PairLevel]
IsLvlPairET.shift_preserves_wf [in DeBrLevel.Datatype.PairLevel]
IsLvlPairET.shift_unfold_1 [in DeBrLevel.Datatype.PairLevel]
IsLvlPairET.shift_unfold [in DeBrLevel.Datatype.PairLevel]
IsLvlPairET.shift_permute [in DeBrLevel.Datatype.PairLevel]
IsLvlPairET.shift_trans [in DeBrLevel.Datatype.PairLevel]
IsLvlPairET.shift_zero_refl [in DeBrLevel.Datatype.PairLevel]
IsLvlPairET.shift_eq_iff [in DeBrLevel.Datatype.PairLevel]
IsLvlPairET.Wf_weakening [in DeBrLevel.Datatype.PairLevel]
IsLvlPairOTWL.eq_leibniz [in DeBrLevel.Datatype.PairLevel]
IsLvlPairOT.shift_preserves_wf_zero [in DeBrLevel.Datatype.PairLevel]
IsLvlPairOT.shift_preserves_wf_2 [in DeBrLevel.Datatype.PairLevel]
IsLvlPairOT.shift_preserves_wf_gen [in DeBrLevel.Datatype.PairLevel]
IsLvlPairOT.shift_preserves_wf_1 [in DeBrLevel.Datatype.PairLevel]
IsLvlPairOT.shift_preserves_wf [in DeBrLevel.Datatype.PairLevel]
IsLvlPairOT.shift_unfold_1 [in DeBrLevel.Datatype.PairLevel]
IsLvlPairOT.shift_unfold [in DeBrLevel.Datatype.PairLevel]
IsLvlPairOT.shift_permute [in DeBrLevel.Datatype.PairLevel]
IsLvlPairOT.shift_trans [in DeBrLevel.Datatype.PairLevel]
IsLvlPairOT.shift_zero_refl [in DeBrLevel.Datatype.PairLevel]
IsLvlPairOT.shift_eq_iff [in DeBrLevel.Datatype.PairLevel]
IsLvlPairOT.Wf_weakening [in DeBrLevel.Datatype.PairLevel]
IsLvlSet.shift_preserves_wf_2 [in DeBrLevel.Set.SetLevel]
IsLvlSet.shift_preserves_wf_gen [in DeBrLevel.Set.SetLevel]
IsLvlSet.shift_preserves_wf_zero [in DeBrLevel.Set.SetLevel]
IsLvlSet.shift_preserves_wf [in DeBrLevel.Set.SetLevel]
IsLvlSet.shift_preserves_wf_1 [in DeBrLevel.Set.SetLevel]
IsLvlSet.shift_unfold_1 [in DeBrLevel.Set.SetLevel]
IsLvlSet.shift_unfold [in DeBrLevel.Set.SetLevel]
IsLvlSet.shift_permute [in DeBrLevel.Set.SetLevel]
IsLvlSet.shift_trans [in DeBrLevel.Set.SetLevel]
IsLvlSet.shift_zero_refl [in DeBrLevel.Set.SetLevel]
IsLvlSet.shift_diff [in DeBrLevel.Set.SetLevel]
IsLvlSet.shift_inter [in DeBrLevel.Set.SetLevel]
IsLvlSet.shift_eq_iff [in DeBrLevel.Set.SetLevel]
IsLvlSet.shift_remove [in DeBrLevel.Set.SetLevel]
IsLvlSet.shift_notin_iff [in DeBrLevel.Set.SetLevel]
IsLvlSet.shift_in_e [in DeBrLevel.Set.SetLevel]
IsLvlSet.shift_add [in DeBrLevel.Set.SetLevel]
IsLvlSet.shift_in_iff [in DeBrLevel.Set.SetLevel]
IsLvlSet.shift_add_in [in DeBrLevel.Set.SetLevel]
IsLvlSet.shift_add_notin [in DeBrLevel.Set.SetLevel]
IsLvlSet.shift_singleton [in DeBrLevel.Set.SetLevel]
IsLvlSet.shift_empty [in DeBrLevel.Set.SetLevel]
IsLvlSet.shift_Empty [in DeBrLevel.Set.SetLevel]
IsLvlSet.shift_union [in DeBrLevel.Set.SetLevel]
IsLvlSet.Wf_weakening [in DeBrLevel.Set.SetLevel]
IsLvlSet.Wf_in [in DeBrLevel.Set.SetLevel]
IsLvlSet.Wf_singleton_iff [in DeBrLevel.Set.SetLevel]
IsLvlSet.Wf_union_iff [in DeBrLevel.Set.SetLevel]
IsLvlSet.Wf_empty [in DeBrLevel.Set.SetLevel]
IsLvlSet.Wf_add_iff [in DeBrLevel.Set.SetLevel]
IsLvlSet.Wf_unfold [in DeBrLevel.Set.SetLevel]
L
Levels.max_key_Add_max [in DeBrLevel.Set.Levels]Levels.max_key_add_max [in DeBrLevel.Set.Levels]
Levels.max_key_empty [in DeBrLevel.Set.Levels]
Levels.max_key_Empty [in DeBrLevel.Set.Levels]
Levels.max_transpose [in DeBrLevel.Set.Levels]
Levels.new_key_in [in DeBrLevel.Set.Levels]
Levels.new_key_Add_max [in DeBrLevel.Set.Levels]
Levels.new_key_add_max [in DeBrLevel.Set.Levels]
Levels.new_key_empty [in DeBrLevel.Set.Levels]
Levels.new_key_Empty [in DeBrLevel.Set.Levels]
Levels.shift_new_refl [in DeBrLevel.Set.Levels]
Levels.shift_permute_2 [in DeBrLevel.Set.Levels]
Levels.shift_permute_1 [in DeBrLevel.Set.Levels]
Level.eq_leibniz [in DeBrLevel.Core.Level]
Level.gt_neq_nlt [in DeBrLevel.Core.Level]
Level.lt_not_eq [in DeBrLevel.Core.Level]
Level.notWf_is_wf_false [in DeBrLevel.Core.Level]
Level.shift_preserves_wf_zero [in DeBrLevel.Core.Level]
Level.shift_preserves_wf_2 [in DeBrLevel.Core.Level]
Level.shift_preserves_wf_gen [in DeBrLevel.Core.Level]
Level.shift_preserves_wf_1 [in DeBrLevel.Core.Level]
Level.shift_preserves_wf [in DeBrLevel.Core.Level]
Level.shift_le [in DeBrLevel.Core.Level]
Level.shift_gt_iff [in DeBrLevel.Core.Level]
Level.shift_unfold_1 [in DeBrLevel.Core.Level]
Level.shift_unfold [in DeBrLevel.Core.Level]
Level.shift_permute_2 [in DeBrLevel.Core.Level]
Level.shift_permute_1 [in DeBrLevel.Core.Level]
Level.shift_permute [in DeBrLevel.Core.Level]
Level.shift_trans [in DeBrLevel.Core.Level]
Level.shift_wf_refl [in DeBrLevel.Core.Level]
Level.shift_zero_refl [in DeBrLevel.Core.Level]
Level.shift_eq_iff [in DeBrLevel.Core.Level]
Level.shift_neq_1 [in DeBrLevel.Core.Level]
Level.shift_neq [in DeBrLevel.Core.Level]
Level.Wf_weakening [in DeBrLevel.Core.Level]
Level.Wf_is_wf_true [in DeBrLevel.Core.Level]
M
MapETLVL.max_key_add_in [in DeBrLevel.Map.Mapkit.MapExt]MapETLVL.max_key_Submap [in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.max_key_in [in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.max_key_add_max_key [in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.max_key_notin [in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.max_key_ub [in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.max_key_add_iff [in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.max_key_add_r [in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.max_key_add_l [in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.max_key_add_max [in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.max_key_Add_r [in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.max_key_Add_l [in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.max_key_Add_max [in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.max_key_empty [in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.max_key_Empty [in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.max_key_diamond [in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.new_key_Submap_add [in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.new_key_Submap [in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.new_key_in [in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.new_key_notin [in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.new_key_add_new_key [in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.new_key_Add_r [in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.new_key_Add_l [in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.new_key_add_in [in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.new_key_add_r [in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.new_key_add_l [in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.new_key_geq_max_key [in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.new_key_add_max [in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.new_key_Add_max [in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.new_key_empty [in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.new_key_Empty [in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.new_key_unfold [in DeBrLevel.Map.Mapkit.MapExt]
MapET.add_shadow [in DeBrLevel.Map.Mapkit.MapExt]
MapET.add_remove [in DeBrLevel.Map.Mapkit.MapExt]
MapET.Empty_eq [in DeBrLevel.Map.Mapkit.MapExt]
MapET.For_all_add_notin [in DeBrLevel.Map.Mapkit.MapExt]
MapET.For_all_add [in DeBrLevel.Map.Mapkit.MapExt]
MapET.For_all_Empty [in DeBrLevel.Map.Mapkit.MapExt]
MapET.For_all_empty [in DeBrLevel.Map.Mapkit.MapExt]
MapET.is_empty_add [in DeBrLevel.Map.Mapkit.MapExt]
MapET.is_empty_Add [in DeBrLevel.Map.Mapkit.MapExt]
MapET.notEmpty_find [in DeBrLevel.Map.Mapkit.MapExt]
MapET.notEmpty_Add [in DeBrLevel.Map.Mapkit.MapExt]
MapET.Submap_find [in DeBrLevel.Map.Mapkit.MapExt]
MapET.Submap_notin [in DeBrLevel.Map.Mapkit.MapExt]
MapET.Submap_in [in DeBrLevel.Map.Mapkit.MapExt]
MapET.Submap_add_2 [in DeBrLevel.Map.Mapkit.MapExt]
MapET.Submap_add_1 [in DeBrLevel.Map.Mapkit.MapExt]
MapET.Submap_add [in DeBrLevel.Map.Mapkit.MapExt]
MapET.Submap_Add_1 [in DeBrLevel.Map.Mapkit.MapExt]
MapET.Submap_Add_find [in DeBrLevel.Map.Mapkit.MapExt]
MapET.Submap_Add_in [in DeBrLevel.Map.Mapkit.MapExt]
MapET.Submap_Add [in DeBrLevel.Map.Mapkit.MapExt]
MapET.Submap_empty_bot [in DeBrLevel.Map.Mapkit.MapExt]
MapET.Submap_Empty [in DeBrLevel.Map.Mapkit.MapExt]
MapET.Submap_Empty_bot [in DeBrLevel.Map.Mapkit.MapExt]
S
SetOTWithLeibniz.add_shadow_leibniz [in DeBrLevel.Set.Setkit.SetOTwL]SetOTWithLeibniz.add_notin_spec [in DeBrLevel.Set.Setkit.SetOTwL]
SetOTWithLeibniz.add_eq_leibniz [in DeBrLevel.Set.Setkit.SetOTwL]
SetOTWithLeibniz.Add_inv [in DeBrLevel.Set.Setkit.SetOTwL]
SetOTWithLeibniz.diff_notin_spec [in DeBrLevel.Set.Setkit.SetOTwL]
SetOTWithLeibniz.diff_notin_add_spec [in DeBrLevel.Set.Setkit.SetOTwL]
SetOTWithLeibniz.diff_in_add_spec [in DeBrLevel.Set.Setkit.SetOTwL]
SetOTWithLeibniz.eqb_refl [in DeBrLevel.Set.Setkit.SetOTwL]
SetOTWithLeibniz.gt_neq_nlt [in DeBrLevel.Set.Setkit.SetOTwL]
SetOTWithLeibniz.inter_notin_add_spec [in DeBrLevel.Set.Setkit.SetOTwL]
SetOTWithLeibniz.inter_in_add_spec [in DeBrLevel.Set.Setkit.SetOTwL]
SetOTWithLeibniz.ltb_lt [in DeBrLevel.Set.Setkit.SetOTwL]
SetOTWithLeibniz.map_union_spec [in DeBrLevel.Set.Setkit.SetOTwL]
SetOTWithLeibniz.map_add_in_spec [in DeBrLevel.Set.Setkit.SetOTwL]
SetOTWithLeibniz.map_add_notin_spec [in DeBrLevel.Set.Setkit.SetOTwL]
SetOTWithLeibniz.map_in_spec [in DeBrLevel.Set.Setkit.SetOTwL]
SetOTWithLeibniz.map_singleton_spec [in DeBrLevel.Set.Setkit.SetOTwL]
SetOTWithLeibniz.map_empty_spec [in DeBrLevel.Set.Setkit.SetOTwL]
SetOTWithLeibniz.map_Empty_spec [in DeBrLevel.Set.Setkit.SetOTwL]
SetOTWithLeibniz.singleton_notin_spec [in DeBrLevel.Set.Setkit.SetOTwL]
SetOTWithLeibniz.transpose_1 [in DeBrLevel.Set.Setkit.SetOTwL]
SetOTWithLeibniz.union_sym_leibniz [in DeBrLevel.Set.Setkit.SetOTwL]
SetOTWithLeibniz.union_notin_spec [in DeBrLevel.Set.Setkit.SetOTwL]
SetOTWithLeibniz.union_add_spec [in DeBrLevel.Set.Setkit.SetOTwL]
Axiom Index
D
DecidableTypeWithLeibniz.eq_leibniz [in DeBrLevel.Core.LevelInterface]E
EqualityTypeWithLeibniz.eq_leibniz [in DeBrLevel.Core.LevelInterface]H
HasShift.shift [in DeBrLevel.Core.LevelInterface]I
IsBdlLvlMapKDInterface.shift_wf_refl [in DeBrLevel.Map.MapLevelInterface]IsBdlLvlMapKDInterface.shift_find_Wf [in DeBrLevel.Map.MapLevelInterface]
IsBdlLvlMapKDInterface.Wf_in_iff [in DeBrLevel.Map.MapLevelInterface]
IsBdlLvlMapKInterface.shift_wf_refl [in DeBrLevel.Map.MapLevelInterface]
IsBdlLvlMapKInterface.shift_find_Wf [in DeBrLevel.Map.MapLevelInterface]
IsBdlLvlMapKInterface.Wf_in_iff [in DeBrLevel.Map.MapLevelInterface]
IsBdlLvlSetInterface.shift_wf_refl [in DeBrLevel.Set.SetLevelInterface]
IsBdlLvlSetInterface.Wf_in_iff [in DeBrLevel.Set.SetLevelInterface]
IsBindlessLeveledEx.shift_wf_refl [in DeBrLevel.Core.LevelInterface]
IsBindlessLeveled.shift_wf_refl [in DeBrLevel.Core.LevelInterface]
IsLvlSetLVLInterface.max_key [in DeBrLevel.Set.SetLevelInterface]
IsLvlSetLVLInterface.new_key [in DeBrLevel.Set.SetLevelInterface]
IsWFb.is_wf [in DeBrLevel.Core.LevelInterface]
IsWF.Wf [in DeBrLevel.Core.LevelInterface]
IsWF.Wf_weakening [in DeBrLevel.Core.LevelInterface]
M
MapInterface.For_all [in DeBrLevel.Map.Mapkit.MapExtInterface]MapInterface.Submap [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.max_key [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.new_key [in DeBrLevel.Map.Mapkit.MapExtInterface]
O
OrderedTypeWithLeibniz.eq_leibniz [in DeBrLevel.Core.LevelInterface]S
SetOTWithLeibnizInterface.ltb [in DeBrLevel.Set.Setkit.SetOTwLInterface]SetOTWithLeibnizInterface.map [in DeBrLevel.Set.Setkit.SetOTwLInterface]
Instance Index
H
HasShift.shift_eq [in DeBrLevel.Core.LevelInterface]I
IsLvlFullOptET.is_wf_eq [in DeBrLevel.Datatype.OptionLevel]IsLvlFullPairET.is_wf_eq [in DeBrLevel.Datatype.PairLevel]
IsLvlFullSet.is_wf_eq [in DeBrLevel.Set.SetLevel]
IsLvlListETWL.eq_equiv [in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.eq_trans [in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.eq_sym [in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.eq_refl [in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.shift_eq [in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.Wf_iff [in DeBrLevel.Datatype.ListLevel]
IsLvlMapD.iff_equiv [in DeBrLevel.Map.MapLevelD]
IsLvlMapD.logic_eq_equiv [in DeBrLevel.Map.MapLevelD]
IsLvlMapD.shift_eq [in DeBrLevel.Map.MapLevelD]
IsLvlMapD.shift_proper [in DeBrLevel.Map.MapLevelD]
IsLvlMapD.Wf_iff [in DeBrLevel.Map.MapLevelD]
IsLvlMapD.Wf_func_iff [in DeBrLevel.Map.MapLevelD]
IsLvlMapKD.iff_equiv [in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.logic_eq_equiv [in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_eq [in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_proper [in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.Wf_iff [in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.Wf_func_iff [in DeBrLevel.Map.MapLevelKD]
IsLvlMapK.iff_equiv [in DeBrLevel.Map.MapLevelK]
IsLvlMapK.logic_eq_equiv [in DeBrLevel.Map.MapLevelK]
IsLvlMapK.shift_eq [in DeBrLevel.Map.MapLevelK]
IsLvlMapK.shift_proper [in DeBrLevel.Map.MapLevelK]
IsLvlMapK.Wf_iff [in DeBrLevel.Map.MapLevelK]
IsLvlMapK.WF_func_iff [in DeBrLevel.Map.MapLevelK]
IsLvlOptET.eq_equiv [in DeBrLevel.Datatype.OptionLevel]
IsLvlOptET.eq_trans [in DeBrLevel.Datatype.OptionLevel]
IsLvlOptET.eq_sym [in DeBrLevel.Datatype.OptionLevel]
IsLvlOptET.eq_refl [in DeBrLevel.Datatype.OptionLevel]
IsLvlOptET.shift_eq [in DeBrLevel.Datatype.OptionLevel]
IsLvlOptET.Wf_iff [in DeBrLevel.Datatype.OptionLevel]
IsLvlPairET.eq_equiv [in DeBrLevel.Datatype.PairLevel]
IsLvlPairET.eq_trans [in DeBrLevel.Datatype.PairLevel]
IsLvlPairET.eq_sym [in DeBrLevel.Datatype.PairLevel]
IsLvlPairET.eq_refl [in DeBrLevel.Datatype.PairLevel]
IsLvlPairET.shift_eq [in DeBrLevel.Datatype.PairLevel]
IsLvlPairET.Wf_iff [in DeBrLevel.Datatype.PairLevel]
IsLvlPairOT.shift_eq [in DeBrLevel.Datatype.PairLevel]
IsLvlPairOT.Wf_iff [in DeBrLevel.Datatype.PairLevel]
IsLvlSetLVLInterface.max_key_eq [in DeBrLevel.Set.SetLevelInterface]
IsLvlSetLVLInterface.new_key_eq [in DeBrLevel.Set.SetLevelInterface]
IsLvlSet.shift_eq [in DeBrLevel.Set.SetLevel]
IsLvlSet.Wf_iff [in DeBrLevel.Set.SetLevel]
IsWFb.is_wf_eq [in DeBrLevel.Core.LevelInterface]
IsWF.Wf_iff [in DeBrLevel.Core.LevelInterface]
L
Levels.logic_eq [in DeBrLevel.Set.Levels]Levels.max_key_eq [in DeBrLevel.Set.Levels]
Levels.max_eq [in DeBrLevel.Set.Levels]
Levels.new_key_eq [in DeBrLevel.Set.Levels]
Level.is_wf_eq [in DeBrLevel.Core.Level]
Level.shift_eq [in DeBrLevel.Core.Level]
Level.Wf_iff [in DeBrLevel.Core.Level]
M
MapETLVL.max_key_eq [in DeBrLevel.Map.Mapkit.MapExt]MapETLVL.max_key_proper_forall [in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.max_key_proper [in DeBrLevel.Map.Mapkit.MapExt]
MapETLVL.new_key_eq [in DeBrLevel.Map.Mapkit.MapExt]
MapET.Add_eq_iff [in DeBrLevel.Map.Mapkit.MapExt]
MapET.Empty_eq_iff [in DeBrLevel.Map.Mapkit.MapExt]
MapET.eq_equiv [in DeBrLevel.Map.Mapkit.MapExt]
MapET.For_all_proper [in DeBrLevel.Map.Mapkit.MapExt]
MapET.iff_equiv [in DeBrLevel.Map.Mapkit.MapExt]
MapET.logic_eq_equiv [in DeBrLevel.Map.Mapkit.MapExt]
MapET.Submap_po [in DeBrLevel.Map.Mapkit.MapExt]
MapET.Submap_trans [in DeBrLevel.Map.Mapkit.MapExt]
MapET.Submap_eq [in DeBrLevel.Map.Mapkit.MapExt]
MapET.Submap_refl [in DeBrLevel.Map.Mapkit.MapExt]
MapInterface.Add_eq_iff [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.Empty_eq_iff [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.eq_equiv [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.For_all_proper [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.Submap_po [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.Submap_eq [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.Submap_trans [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.Submap_refl [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.max_key_eq [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapLVLInterface.new_key_eq [in DeBrLevel.Map.Mapkit.MapExtInterface]
S
SetOTWithLeibnizInterface.proper_1 [in DeBrLevel.Set.Setkit.SetOTwLInterface]SetOTWithLeibniz.proper_1 [in DeBrLevel.Set.Setkit.SetOTwL]
Section Index
H
HasShift.specs [in DeBrLevel.Core.LevelInterface]I
IsLeveled.specs [in DeBrLevel.Core.LevelInterface]IsLvlFullListETWL.props [in DeBrLevel.Datatype.ListLevel]
IsLvlFullOptET.definition [in DeBrLevel.Datatype.OptionLevel]
IsLvlFullOptET.valid [in DeBrLevel.Datatype.OptionLevel]
IsLvlFullPairET.is_wf [in DeBrLevel.Datatype.PairLevel]
IsLvlFullPairOT.is_wf [in DeBrLevel.Datatype.PairLevel]
IsLvlListETWL.shift_props [in DeBrLevel.Datatype.ListLevel]
IsLvlMapDInterface.specs [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKDInterface.specs [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapKInterface.specs [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLDInterface.props [in DeBrLevel.Map.MapLevelInterface]
IsLvlMapLVLInterface.specs [in DeBrLevel.Map.MapLevelInterface]
IsLvlOptET.definition [in DeBrLevel.Datatype.OptionLevel]
IsLvlOptET.shift [in DeBrLevel.Datatype.OptionLevel]
IsLvlPairET.shift [in DeBrLevel.Datatype.PairLevel]
IsLvlPairOT.shift [in DeBrLevel.Datatype.PairLevel]
IsLvlSetInterface.specs [in DeBrLevel.Set.SetLevelInterface]
IsLvlSetLVLInterface.specifications [in DeBrLevel.Set.SetLevelInterface]
IsLvlSet.specs [in DeBrLevel.Set.SetLevel]
IsWFFull.specs [in DeBrLevel.Core.LevelInterface]
L
Level.lt_eq [in DeBrLevel.Core.Level]Level.shift [in DeBrLevel.Core.Level]
M
MapInterface.specifications [in DeBrLevel.Map.Mapkit.MapExtInterface]MapLVLInterface.specs [in DeBrLevel.Map.Mapkit.MapExtInterface]
S
SetOTWithLeibnizInterface.specs [in DeBrLevel.Set.Setkit.SetOTwLInterface]SetOTWithLeibniz.props [in DeBrLevel.Set.Setkit.SetOTwL]
Definition Index
I
IsLvlFullListETWL.is_wf [in DeBrLevel.Datatype.ListLevel]IsLvlFullOptET.is_wf [in DeBrLevel.Datatype.OptionLevel]
IsLvlFullPairET.is_wf [in DeBrLevel.Datatype.PairLevel]
IsLvlFullPairOT.is_wf [in DeBrLevel.Datatype.PairLevel]
IsLvlFullSet.is_wf [in DeBrLevel.Set.SetLevel]
IsLvlListETWL.eq [in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.shift [in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.t [in DeBrLevel.Datatype.ListLevel]
IsLvlListETWL.Wf [in DeBrLevel.Datatype.ListLevel]
IsLvlMapD.shift [in DeBrLevel.Map.MapLevelD]
IsLvlMapD.shift_func [in DeBrLevel.Map.MapLevelD]
IsLvlMapD.Wf [in DeBrLevel.Map.MapLevelD]
IsLvlMapD.Wf_func [in DeBrLevel.Map.MapLevelD]
IsLvlMapKD.shift [in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.shift_func [in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.Wf [in DeBrLevel.Map.MapLevelKD]
IsLvlMapKD.Wf_func [in DeBrLevel.Map.MapLevelKD]
IsLvlMapK.shift [in DeBrLevel.Map.MapLevelK]
IsLvlMapK.shift_func [in DeBrLevel.Map.MapLevelK]
IsLvlMapK.Wf [in DeBrLevel.Map.MapLevelK]
IsLvlMapK.Wf_func [in DeBrLevel.Map.MapLevelK]
IsLvlOptET.eq [in DeBrLevel.Datatype.OptionLevel]
IsLvlOptET.shift [in DeBrLevel.Datatype.OptionLevel]
IsLvlOptET.t [in DeBrLevel.Datatype.OptionLevel]
IsLvlOptET.Wf [in DeBrLevel.Datatype.OptionLevel]
IsLvlPairET.eq [in DeBrLevel.Datatype.PairLevel]
IsLvlPairET.shift [in DeBrLevel.Datatype.PairLevel]
IsLvlPairET.t [in DeBrLevel.Datatype.PairLevel]
IsLvlPairET.Wf [in DeBrLevel.Datatype.PairLevel]
IsLvlPairOT.shift [in DeBrLevel.Datatype.PairLevel]
IsLvlPairOT.Wf [in DeBrLevel.Datatype.PairLevel]
IsLvlSetInterface.compare [in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.compare_spec [in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.eq [in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.eq_leibniz [in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.eq_dec [in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.eq_equiv [in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.lt [in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.lt_compat [in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.lt_strorder [in DeBrLevel.Set.SetLevelInterface]
IsLvlSetInterface.t [in DeBrLevel.Set.SetLevelInterface]
IsLvlSet.compare [in DeBrLevel.Set.SetLevel]
IsLvlSet.compare_spec [in DeBrLevel.Set.SetLevel]
IsLvlSet.eq [in DeBrLevel.Set.SetLevel]
IsLvlSet.eq_leibniz [in DeBrLevel.Set.SetLevel]
IsLvlSet.eq_dec [in DeBrLevel.Set.SetLevel]
IsLvlSet.eq_equiv [in DeBrLevel.Set.SetLevel]
IsLvlSet.lt [in DeBrLevel.Set.SetLevel]
IsLvlSet.lt_compat [in DeBrLevel.Set.SetLevel]
IsLvlSet.lt_strorder [in DeBrLevel.Set.SetLevel]
IsLvlSet.shift [in DeBrLevel.Set.SetLevel]
IsLvlSet.t [in DeBrLevel.Set.SetLevel]
IsLvlSet.Wf [in DeBrLevel.Set.SetLevel]
L
Levels.max_key [in DeBrLevel.Set.Levels]Levels.new_key [in DeBrLevel.Set.Levels]
Level.is_wf [in DeBrLevel.Core.Level]
Level.shift [in DeBrLevel.Core.Level]
Level.Wf [in DeBrLevel.Core.Level]
M
MapETLVL.max_key [in DeBrLevel.Map.Mapkit.MapExt]MapETLVL.new_key [in DeBrLevel.Map.Mapkit.MapExt]
MapET.eq [in DeBrLevel.Map.Mapkit.MapExt]
MapET.For_all [in DeBrLevel.Map.Mapkit.MapExt]
MapET.Submap [in DeBrLevel.Map.Mapkit.MapExt]
MapET.t [in DeBrLevel.Map.Mapkit.MapExt]
MapInterface.eq [in DeBrLevel.Map.Mapkit.MapExtInterface]
MapInterface.t [in DeBrLevel.Map.Mapkit.MapExtInterface]
S
SetOTWithLeibniz.ltb [in DeBrLevel.Set.Setkit.SetOTwL]SetOTWithLeibniz.map [in DeBrLevel.Set.Setkit.SetOTwL]
| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1106 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (178 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (320 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (18 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (389 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (25 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (81 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (27 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (68 entries) |