gistfile1.txt

Theorem darin : [{X:U{i}} {Y:U{i}} {a:X}{b:Y}{c:X}{d:Y} =(<a,b>;<c,d>;X*Y) => =(a;c;X) * =(b;d;Y)] {
  auto;
  [ assert [=(a;spread(<a,b>; x._.x); X)];
      [reduce; auto, hyp-subst -> #8 [h.=(h;c;X)]; auto];

    assert [=(c;spread(<c,d>;x.y.x); X)];
      [reduce; auto, hyp-subst -> #9 [h.=(spread(<a,b>; x._.x); h; X)]; auto];

    eq-cd [h.X, X*Y]; auto

  , assert [=(b;spread(<a,b>; _.y.y); Y)];
    [reduce; auto, hyp-subst -> #8 [h.=(h;d;Y)]; auto];

    assert [=(d;spread(<c,d>; _.y.y); Y)];
    [reduce; auto, hyp-subst -> #9 [h.=(spread(<a,b>;_.y.y);h;Y)]; auto];

    eq-cd [h.Y, X*Y]; auto
  ]
}.