gistfile1.txt

Theorem prod_obj_eq : [
  ∀(RawCatSig; RC.
  ∀(RawCatSig; RD.
  ∀(ap(obj; RC); CA. ∀(ap(obj; RC); CB.
  ∀(ap(obj; RD); DA. ∀(ap(obj; RD); DB.
  ∀(=(CA; CB; ap(obj; RC)); fst.
  ∀(=(DA; DB; ap(obj; RD)); snd.
    =(pair(CA; DA); pair(CB; DB); Σ(ap(obj; RC); _. ap(obj; RD)))))))))))
] {
  auto; isect-intro @1;
  [ isect-intro @1;
    [ auto; refine <rawcat_unfold>; auto
    , lemma <RawCatSig_wf>
    ]
  , lemma <RawCatSig_wf>
  ].
}.