proposition: Lemma vee_maps_tack : tack (R i1) (tack (R i2) (tack (R i3) (tack (R a12) (tack (R a32) emptyset)))) = vee_maps.
proof: Proof. ap extensionality; uhg; ir. rwi tack_inc H. nin H. rwi tack_inc H. nin H. rwi tack_inc H. nin H. rwi tack_inc H. nin H. rwi tack_inc H. nin H. nin H. nin x0. rw H. ap R_inc. rw H. ap R_inc. rw H. ap R_inc. rw H. ap R_inc. rw H. ap R_inc. rw tack_inc. rw tack_inc. rw tack_inc. rw tack_inc. nin H. wr H. nin x0. ap or_intror. tv. ap or_introl; ap or_intror; tv. ap or_introl; ap or_introl; ap or_intror; tv. ap or_introl; ap or_introl; ap or_introl. ap or_intror; tv. ap or_introl; ap or_introl; ap or_introl; ap or_introl. rw tack_inc. ap or_intror; tv. Qed.
imports: Arith cat_examples cardinal fc_limits