- | intros; intros 2; simplify;
- letin xxx ≝ (comp BP); clearbody xxx; unfold BP in xxx:(?→?→?→?→?→%); simplify in xxx;
- unfold basic_pair in xxx; simplify in xxx;
- ]
-*)
\ No newline at end of file
+ | intros;
+ change with (a ∘ b = a' ∘ b');
+ change in H with (rp'' ?? a = rp'' ?? a');
+ change in H1 with (rp'' ?? b = rp ?? b');
+ apply (.= (H‡H1));
+ apply refl1]
+ | intros; simplify;
+ change with ((a12 ∘ a23) ∘ a34 = a12 ∘ (a23 ∘ a34));
+ apply (.= ASSOC1);
+ apply refl1
+ | intros; simplify;
+ change with (id o1 ∘ a = a);*)
\ No newline at end of file