proposition: Lemma reflect_false_inv P Q : reflect P Q false -> Q.
proof: Proof. exact (fun x => match x in reflect _ _ b return if b then ID else Q with | reflect_true _ _ H => fun _ x => x | reflect_false _ _ H => H end). Qed.