vstd::pervasive

Function proof_from_false

Source 
pub proof fn proof_from_false<A>() -> tracked a : A
Expand description
requires
false,