Write the proofs for the following propositions in Agda:
“`
R -> (not Q -> S) -> (Q and R -> not R) -> S
(not P or Q) -> not (P and not Q)
“`
## Solutions
“`
as1q1 : {Q R S : Prop} -> R -> (not Q -> S) -> (Q and R -> not R) -> S
as1q1 {Q} {R} {S} r f g = s where
nq : not Q
nq q = b where
qr : Q and R
qr = andI q r
nr : not R
nr = g qr
b : Falsity
b = nr r
s : S
s = f nq
as1q2 : {P Q : Prop} -> (not P or Q) -> not (P and not Q)
as1q2 {P} {Q} npq = npnq where
npnq : not (P and not Q)
npnq pnq = b where
p : P
p = andEl pnq
nq : not Q
nq = andEr pnq
or1 : not P -> Falsity
or1 np = np p
or2 : Q -> Falsity
or2 q = nq q
b : Falsity
b = orE npq or1 or2
“`