| elim (frees_inv_pair … H) -H #f #Hf #H destruct
/4 width=7 by drops_refl, or3_intro1, ex3_4_intro/
| elim (frees_inv_lref … H) -H #f #Hf #H destruct
elim (IH … Hf) -IH -Hf *
[ /4 width=3 by drops_drop, or3_intro0, ex3_intro/
| /4 width=7 by drops_drop, or3_intro1, ex3_4_intro/
| elim (frees_inv_pair … H) -H #f #Hf #H destruct
/4 width=7 by drops_refl, or3_intro1, ex3_4_intro/
| elim (frees_inv_lref … H) -H #f #Hf #H destruct
elim (IH … Hf) -IH -Hf *
[ /4 width=3 by drops_drop, or3_intro0, ex3_intro/
| /4 width=7 by drops_drop, or3_intro1, ex3_4_intro/