I am trying to prove that some preconditions don't introduce an inconsistency to my (constructive) system. I would like to know if this is possible with the set-up below, and how to do this, and what additionally i need to include/specify to make this happen. What do I need to specify about isThisTrue?
Inductive myThing : Type :=
| a : myThing
| b : myThing.
Inductive isThisTrue : myThing -> Prop :=
| is_a : isThisTrue a
| is_b : isThisTrue b.
Definition somethingIsTrue := ~ (forall x, ~ isThisTrue x).
Definition nothingIsFalse := forall x, ~~ isThisTrue x.
So, I want show something like -
Definition consistent := somethingIsTrue /\ nothingIsFalse ... does not introduce inconsistency