## Stream: new members

### Topic: Negated proof on else-branch

#### Marcus Rossel (Feb 24 2021 at 20:27):

If-then-else expressions give us the option of obtaining a proof of the condition we're checking on the then-branch:

if h : my_condition
then use_condition h
else ...


Is there a way of obtaining a proof of ¬h on the else-branch?

#### Alex J. Best (Feb 24 2021 at 20:29):

In the else branch the identifier h should refer to a term of type  ¬my_condition

Last updated: May 13 2021 at 21:12 UTC