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