proposition: Lemma vee_obs_tack : tack (R o1) (tack (R o2) (tack (R o3) emptyset)) = vee_obs.
proof: Proof. ap extensionality; uhg; ir. rwi tack_inc H. nin H. rwi tack_inc H. nin H. rwi tack_inc H. nin H. nin H. elim x0. rw H. ap R_inc. rw H. ap R_inc. rw H. ap R_inc. nin H. wr H. nin x0. rw tack_inc. ap or_intror. tv. rw tack_inc. ap or_introl. rw tack_inc. ap or_intror; tv. rw tack_inc. ap or_introl. rw tack_inc. ap or_introl. rw tack_inc. ap or_intror; tv. Qed.
imports: Arith cat_examples cardinal fc_limits