-[ /4 width=3 by fcla_isid, ex2_intro/
-| #f #I #L1 #L2 #_ * >length_bind /3 width=3 by fcla_next, ex2_intro, eq_f/
-| #f #I1 #I2 #L1 #L2 #_ #_ * >length_bind >length_bind /3 width=3 by fcla_push, ex2_intro/
+[ /4 width=3 by pr_fcla_isi, ex2_intro/
+| #f #I #L1 #L2 #_ * >length_bind /3 width=3 by pr_fcla_next, ex2_intro, eq_f/
+| #f #I1 #I2 #L1 #L2 #_ #_ * >length_bind >length_bind /3 width=3 by pr_fcla_push, ex2_intro/