Type checking the impossible statement currently manually scans the context for a false assumption. This can be improved by using proof search instead, for example contradictory assumptions should be sufficient and proof search should know how to apply the contradiction lemma from prelude.
Type checking the impossible statement currently manually scans the context for a false assumption. This can be improved by using proof search instead, for example contradictory assumptions should be sufficient and proof search should know how to apply the contradiction lemma from prelude.