fix(kernel/inductive): bug in eliminator for recursive datatypes in Prop
fix(tests/lean): avoid 'sorry' in expected output