proposition: Lemma semi_reflect_true_inv P : semi_reflect P true -> P.
proof: Proof. exact (fun x => match x in semi_reflect _ b return if b then P else ID with | semi_reflect_true _ H => H | semi_reflect_false _ => (fun _ x => x) end). Qed.