have h9 : betty_beg := h3 h7
case intro.inr
p q r al_ac betty_beg carl_cac : Prop
h2 : betty_beg → ¬al_ac
h3 : carl_cac → betty_beg
h4 : al_ac
h7 : carl_cac
⊢ False
case intro.inr
p q r al_ac betty_beg carl_cac : Prop
h2 : betty_beg → ¬al_ac
h3 : carl_cac → betty_beg
h4 : al_ac
h7 : carl_cac
h9 : betty_beg
⊢ False