Lattice

Statistics

Metric	Count
Definitions	0
Theorems `bagInter`, `bagInter_left`, `bagInter_right`, `dropSlice_inter`, `drop_inter`, `inter_append`, `take_inter`	7
Total	7

Name	Kind	Assumes	Proves	Validates	Depends On
`bagInter` 📖	—	—	—	—	`bagInter_right` `bagInter_left`
`bagInter_left` 📖	—	—	—	—	`List.nil_bagInter` `List.cons_bagInter_of_pos` `List.cons_bagInter_of_neg`
`bagInter_right` 📖	—	—	—	—	—
`dropSlice_inter` 📖	—	—	—	—	`List.dropSlice_eq` `take_inter` `drop_inter` `inter_append`
`drop_inter` 📖	—	—	—	—	`List.inter_reverse` `take_inter`
`inter_append` 📖	—	—	—	—	`List.inter_cons_of_mem` `List.inter_cons_of_notMem`
`take_inter` 📖	—	—	—	—	`List.Nodup.take_eq_filter_mem`

---