Direction from right to left:
We assume
(DA.RA)
and show
(DA.LC) .
We prove (DA.LC) by the deduction rule.
(DA.LC.H)
(DA.LC.C) .
We prove (DA.LC.C) by case distinction using (DA.RA).
Case (DA.RA.1) :
Case (DA.RA.2) :