blob: 8c7d4ac776422fc1d85ec2e69beea51128cd89ba (
plain)
1
2
3
4
5
6
7
8
9
|
negbT: forall [b : bool], b = false -> ~~ b
contra_notN: forall [P : Prop] [b : bool], (b -> P) -> ~ P -> ~~ b
contraPN: forall [P : Prop] [b : bool], (b -> ~ P) -> P -> ~~ b
contraNN: forall [c b : bool], (c -> b) -> ~~ b -> ~~ c
contraL: forall [c b : bool], (c -> ~~ b) -> b -> ~~ c
contraTN: forall [c b : bool], (c -> ~~ b) -> b -> ~~ c
contra: forall [c b : bool], (c -> b) -> ~~ b -> ~~ c
introN: forall [P : Prop] [b : bool], reflect P b -> ~ P -> ~~ b
contraFN: forall [c b : bool], (c -> b) -> b = false -> ~~ c
|
