(** %
# \section{\label{sec:catches}Catches and Repos}
% *)
Module Export catches_commute_consistent_1_7.

Require Import Equality.
Require Import names.
Require Import patch_universes.
Require Import invertible_patchlike.
Require Import invertible_patch_universe.
Require Import contexted_patches.
Require Import catches_definition.

Lemma CatchCommuteConsistent1_7 :
      forall {pu_type : NameSet -> NameSet -> Type}
             {ppu : PartPatchUniverse pu_type pu_type}
             {pui : PatchUniverseInv ppu ppu}
             {pu : PatchUniverse pui}
             {ipl : InvertiblePatchlike pu_type}
             {ipu : InvertiblePatchUniverse pu ipl}
             {o op opq opqr opr oq oqr : NameSet}
             {p1 : Catch ipl o op}
             {q1 : Catch ipl op opq}
             {r1 : Catch ipl opq opqr}
             {q2 : Catch ipl opr opqr}
             {r2 : Catch ipl op opr}
             {q3 : Catch ipl o oq}
             {r3 : Catch ipl oq oqr}
             {p3 : Catch ipl oqr opqr}
             {p5 : Catch ipl oq opq}
             (catchCommuteDetails : <<q1, r1>> <~>7 <<r2, q2>>)
             (commute2 : <<p1, q1>> <~>c <<q3, p5>>)
             (commute3 : <<p5, r1>> <~>c <<r3, p3>>),
      (exists or : NameSet,
       (exists r4 : Catch ipl o or,
        (exists q4 : Catch ipl or oqr,
         (exists p6 : Catch ipl or opr,
          <<q3, r3>> <~>c <<r4, q4>> /\
          <<p1, r2>> <~>c <<r4, p6>> /\
          <<p6, q2>> <~>c <<q4, p3>>)))).
Proof with auto.
intros.
dependent destruction catchCommuteDetails;
destruct commute2;
try (abstract (dependent destruction catchCommuteDetails));
dependent destruction catchCommuteDetails;
destruct commute3;
try (abstract (dependent destruction catchCommuteDetails));
dependent destruction catchCommuteDetails.
                    (* case 7/1/7 *)
                    admit.
                (* case 7/2/7 *)
                admit.
            (* case 7/3/7 *)
            admit.
        (* case 7/4/7 *)
        admit.
    (* case 7/6/5 *)
    admit.
(* case 7/8/7 *)
admit.
Qed.

End catches_commute_consistent_1_7.