proposition: Lemma noconf_noc {A} {w x y z : A} {p q r s} (u v : Square w x y z p q r s) (f : noc u v) : u = v.
proof: Proof. depelim u. revert f. generalize_eqs_sig v. destruct v. simpl. simpl. simplify ?. simpl. simplify ?. simpl. intros e. intros e'. rewrite <- e'. clear e'. depelim e. destruct e''2. destruct e''3. destruct e''4. rewrite <- H in f. exact I. Defined.
imports: Equations(Equations)