proposition: Fact K2'_injective x y z a b a' b' : K2' x y z a b = K2' x y z a' b' -> (a,b) = (a',b').
proof: Proof. intros h. pose proof (ap (K'K _ _) h). simp K'K in H. noconf H. depelim H. cbn in h. Fact K2_injective x y z w a b a' b' eq eq': K2 x y z w eq a b = K2 x y z w eq' a' b' -> (a,b) = (a',b'). Proof. intros h. pose proof (ap (KK' _ _) h). cbn in H. apply K_equiv in h. intros h%(noConfusionHom_K_obligation_2 _ _). simpl in h. depelim h. destruct h1'1. destruct eq. destruct h as [yy' [zz' [aa' bb']]]. rewrite (UIP_refl_nat _ yy') in aa', bb'. rewrite (UIP_refl_nat _ zz') in bb'. rewrite <- aa', <- bb'. reflexivity. Qed.
imports: Equations(Equations)