Prove filter_map in List.v
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?
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?