Skip to content

Prove filter_map in List.v

gaxi requested to merge filter_map-List.v into master

I found that filter_map can be proved by assuming transitivity of R_a. Should I change proposition and prove it? Or should I keep it Admitted?

Merge request reports