+ '[' 0 -eq 1 ']'
+ echo 'Doing: timeout --foreground --kill-after=5 --signal=SIGINT 121 time metta /opt/logicmoo_opencog/hyperon-wam/examples/baseline_compat/hyperon-pln_metta/subtyping/subtyping-test.metta'
Doing: timeout --foreground --kill-after=5 --signal=SIGINT 121 time metta /opt/logicmoo_opencog/hyperon-wam/examples/baseline_compat/hyperon-pln_metta/subtyping/subtyping-test.metta
+ eval 'timeout --foreground --kill-after=5 --signal=SIGINT 121 time metta /opt/logicmoo_opencog/hyperon-wam/examples/baseline_compat/hyperon-pln_metta/subtyping/subtyping-test.metta'
++ timeout --foreground --kill-after=5 --signal=SIGINT 121 time metta /opt/logicmoo_opencog/hyperon-wam/examples/baseline_compat/hyperon-pln_metta/subtyping/subtyping-test.metta
[()]
[()]
[()]
[(let* (((: felix Mammal) (synthesize (: felix Mammal) kb rb Z))) (: (coerce STRefl felix) Mammal)), (: (coerce CM felix) Mammal)]
[(let* (((: $proof2#3269 (: felix Mammal)) (synthesize (: $proof2#3269 (: felix Mammal)) kb rb Z))) (: (STImplCoer STRefl $proof2#3269) (: felix Mammal))), (: (STImplCoer CM fC) (: felix Mammal)), (let* (((: $proof2#3673 (: felix Mammal)) (synthesize (: $proof2#3673 (: felix Mammal)) kb rb Z))) (: (coerce STRefl $proof2#3673) (: felix Mammal)))]
[(let* (((: $proof2#5039 (<: Cat Animal)) (synthesize (: $proof2#5039 (<: Cat Animal)) kb rb Z))) (: (STTrans STRefl $proof2#5039) (<: Cat Animal))), (: (STTrans CM MA) (<: Cat Animal)), (let* (((: $proof2#5473 (<: Cat Animal)) (synthesize (: $proof2#5473 (<: Cat Animal)) kb rb Z))) (: (coerce STRefl $proof2#5473) (<: Cat Animal)))]
[(let* (((: felix Animal) (synthesize (: felix Animal) kb rb (S Z)))) (: (coerce STRefl felix) Animal)), (let* (((: felix Mammal) (synthesize (: felix Mammal) kb rb (S Z)))) (: (coerce MA felix) Animal)), (let* (((: felix Animal) (synthesize (: felix Animal) kb rb (S Z)))) (: (coerce (STTrans STRefl STRefl) felix) Animal)), (let* (((: felix Mammal) (synthesize (: felix Mammal) kb rb (S Z)))) (: (coerce (STTrans STRefl MA) felix) Animal)), (: (coerce (STTrans CM MA) felix) Animal), (let* (((: felix Mammal) (synthesize (: felix Mammal) kb rb (S Z)))) (: (coerce (STTrans MA STRefl) felix) Animal)), (let* (((: felix Animal) (synthesize (: felix Animal) kb rb (S Z)))) (: (coerce (coerce STRefl STRefl) felix) Animal)), (let* (((: felix Mammal) (synthesize (: felix Mammal) kb rb (S Z)))) (: (coerce (coerce STRefl MA) felix) Animal))]
[(: (STImplCoer MA (STImplCoer CM fC)) (: felix Animal)), (: (STImplCoer (STTrans STRefl MA) (STImplCoer CM fC)) (: felix Animal)), (: (STImplCoer (STTrans CM MA) fC) (: felix Animal)), (: (STImplCoer (STTrans CM MA) (STImplCoer STRefl fC)) (: felix Animal)), (: (STImplCoer (STTrans CM MA) (coerce STRefl fC)) (: felix Animal)), (: (STImplCoer (STTrans MA STRefl) (STImplCoer CM fC)) (: felix Animal)), (: (STImplCoer (coerce STRefl MA) (STImplCoer CM fC)) (: felix Animal))]
[(let* (((: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) (synthesize (: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) kb rb (S (S Z))))) (: (STTrans STRefl $proof2#20647) (<: (-> Physical Weight) (-> Cat Weight)))), (let* (((: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) (synthesize (: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) kb rb (S (S Z))))) (: (STTrans (STTrans STRefl STRefl) $proof2#20647) (<: (-> Physical Weight) (-> Cat Weight)))), (let* (((: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) (synthesize (: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) kb rb (S (S Z))))) (: (STTrans (STTrans STRefl (STTrans STRefl STRefl)) $proof2#20647) (<: (-> Physical Weight) (-> Cat Weight)))), (let* (((: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) (synthesize (: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) kb rb (S (S Z))))) (: (STTrans (STTrans STRefl (STFnTy STRefl STRefl)) $proof2#20647) (<: (-> Physical Weight) (-> Cat Weight)))), (: (STTrans (STTrans STRefl (STFnTy AP STRefl)) (STTrans (STFnTy MA STRefl) (STFnTy CM STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STTrans STRefl (STFnTy AP STRefl)) (STFnTy (STTrans CM MA) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STTrans STRefl (STFnTy AP STRefl)) (STFnTy (STTrans CM MA) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STTrans STRefl (STFnTy AP STRefl)) (STFnTy (STTrans CM MA) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (let* (((: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) (synthesize (: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) kb rb (S (S Z))))) (: (STTrans (STTrans STRefl (coerce STRefl STRefl)) $proof2#20647) (<: (-> Physical Weight) (-> Cat Weight)))), (let* (((: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) (synthesize (: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) kb rb (S (S Z))))) (: (STTrans (STTrans (STTrans STRefl STRefl) STRefl) $proof2#20647) (<: (-> Physical Weight) (-> Cat Weight)))), (let* (((: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) (synthesize (: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) kb rb (S (S Z))))) (: (STTrans (STTrans (STTrans STRefl STRefl) (STTrans STRefl STRefl)) $proof2#20647) (<: (-> Physical Weight) (-> Cat Weight)))), (let* (((: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) (synthesize (: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) kb rb (S (S Z))))) (: (STTrans (STTrans (STTrans STRefl STRefl) (STFnTy STRefl STRefl)) $proof2#20647) (<: (-> Physical Weight) (-> Cat Weight)))), (: (STTrans (STTrans (STTrans STRefl STRefl) (STFnTy AP STRefl)) (STTrans (STFnTy MA STRefl) (STFnTy CM STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STTrans (STTrans STRefl STRefl) (STFnTy AP STRefl)) (STFnTy (STTrans CM MA) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STTrans (STTrans STRefl STRefl) (STFnTy AP STRefl)) (STFnTy (STTrans CM MA) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STTrans (STTrans STRefl STRefl) (STFnTy AP STRefl)) (STFnTy (STTrans CM MA) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (let* (((: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) (synthesize (: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) kb rb (S (S Z))))) (: (STTrans (STTrans (STTrans STRefl STRefl) (coerce STRefl STRefl)) $proof2#20647) (<: (-> Physical Weight) (-> Cat Weight)))), (let* (((: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) (synthesize (: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) kb rb (S (S Z))))) (: (STTrans (STTrans (STFnTy STRefl STRefl) STRefl) $proof2#20647) (<: (-> Physical Weight) (-> Cat Weight)))), (let* (((: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) (synthesize (: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) kb rb (S (S Z))))) (: (STTrans (STTrans (STFnTy STRefl STRefl) (STTrans STRefl STRefl)) $proof2#20647) (<: (-> Physical Weight) (-> Cat Weight)))), (let* (((: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) (synthesize (: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) kb rb (S (S Z))))) (: (STTrans (STTrans (STFnTy STRefl STRefl) (STFnTy STRefl STRefl)) $proof2#20647) (<: (-> Physical Weight) (-> Cat Weight)))), (: (STTrans (STTrans (STFnTy STRefl STRefl) (STFnTy AP STRefl)) (STTrans (STFnTy MA STRefl) (STFnTy CM STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STTrans (STFnTy STRefl STRefl) (STFnTy AP STRefl)) (STFnTy (STTrans CM MA) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STTrans (STFnTy STRefl STRefl) (STFnTy AP STRefl)) (STFnTy (STTrans CM MA) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STTrans (STFnTy STRefl STRefl) (STFnTy AP STRefl)) (STFnTy (STTrans CM MA) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (let* (((: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) (synthesize (: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) kb rb (S (S Z))))) (: (STTrans (STTrans (STFnTy STRefl STRefl) (coerce STRefl STRefl)) $proof2#20647) (<: (-> Physical Weight) (-> Cat Weight)))), (: (STTrans (STTrans (STFnTy AP STRefl) STRefl) (STTrans (STFnTy MA STRefl) (STFnTy CM STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STTrans (STFnTy AP STRefl) STRefl) (STFnTy (STTrans CM MA) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STTrans (STFnTy AP STRefl) STRefl) (STFnTy (STTrans CM MA) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STTrans (STFnTy AP STRefl) STRefl) (STFnTy (STTrans CM MA) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STTrans (STFnTy AP STRefl) (STTrans STRefl STRefl)) (STTrans (STFnTy MA STRefl) (STFnTy CM STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STTrans (STFnTy AP STRefl) (STTrans STRefl STRefl)) (STFnTy (STTrans CM MA) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STTrans (STFnTy AP STRefl) (STTrans STRefl STRefl)) (STFnTy (STTrans CM MA) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STTrans (STFnTy AP STRefl) (STTrans STRefl STRefl)) (STFnTy (STTrans CM MA) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STTrans (STFnTy AP STRefl) (STFnTy STRefl STRefl)) (STTrans (STFnTy MA STRefl) (STFnTy CM STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STTrans (STFnTy AP STRefl) (STFnTy STRefl STRefl)) (STFnTy (STTrans CM MA) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STTrans (STFnTy AP STRefl) (STFnTy STRefl STRefl)) (STFnTy (STTrans CM MA) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STTrans (STFnTy AP STRefl) (STFnTy STRefl STRefl)) (STFnTy (STTrans CM MA) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STTrans (STFnTy AP STRefl) (STFnTy MA STRefl)) (STTrans STRefl (STFnTy CM STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STTrans (STFnTy AP STRefl) (STFnTy MA STRefl)) (STTrans (STTrans STRefl STRefl) (STFnTy CM STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STTrans (STFnTy AP STRefl) (STFnTy MA STRefl)) (STTrans (STFnTy STRefl STRefl) (STFnTy CM STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STTrans (STFnTy AP STRefl) (STFnTy MA STRefl)) (STTrans (STFnTy CM STRefl) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STTrans (STFnTy AP STRefl) (STFnTy MA STRefl)) (STTrans (STFnTy CM STRefl) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STTrans (STFnTy AP STRefl) (STFnTy MA STRefl)) (STTrans (STFnTy CM STRefl) (STFnTy STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STTrans (STFnTy AP STRefl) (STFnTy MA STRefl)) (STTrans (STFnTy CM STRefl) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STTrans (STFnTy AP STRefl) (STFnTy MA STRefl)) (STTrans (coerce STRefl STRefl) (STFnTy CM STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STTrans (STFnTy AP STRefl) (STFnTy MA STRefl)) (STFnTy CM STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STTrans (STFnTy AP STRefl) (STFnTy MA STRefl)) (STFnTy CM (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STTrans (STFnTy AP STRefl) (STFnTy MA STRefl)) (STFnTy CM (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STTrans (STFnTy AP STRefl) (STFnTy MA STRefl)) (STFnTy (STTrans STRefl CM) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STTrans (STFnTy AP STRefl) (STFnTy MA STRefl)) (STFnTy (STTrans STRefl CM) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STTrans (STFnTy AP STRefl) (STFnTy MA STRefl)) (STFnTy (STTrans STRefl CM) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STTrans (STFnTy AP STRefl) (STFnTy MA STRefl)) (STFnTy (STTrans CM STRefl) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STTrans (STFnTy AP STRefl) (STFnTy MA STRefl)) (STFnTy (STTrans CM STRefl) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STTrans (STFnTy AP STRefl) (STFnTy MA STRefl)) (STFnTy (STTrans CM STRefl) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STTrans (STFnTy AP STRefl) (STFnTy MA STRefl)) (STFnTy (coerce STRefl CM) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STTrans (STFnTy AP STRefl) (STFnTy MA STRefl)) (STFnTy (coerce STRefl CM) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STTrans (STFnTy AP STRefl) (STFnTy MA STRefl)) (STFnTy (coerce STRefl CM) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STTrans (STFnTy AP STRefl) (STFnTy MA STRefl)) (coerce STRefl (STFnTy CM STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STTrans (STFnTy AP STRefl) (STFnTy MA STRefl)) (coerce (STTrans STRefl STRefl) (STFnTy CM STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STTrans (STFnTy AP STRefl) (STFnTy MA STRefl)) (coerce (coerce STRefl STRefl) (STFnTy CM STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STTrans (STFnTy AP STRefl) (coerce STRefl STRefl)) (STTrans (STFnTy MA STRefl) (STFnTy CM STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STTrans (STFnTy AP STRefl) (coerce STRefl STRefl)) (STFnTy (STTrans CM MA) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STTrans (STFnTy AP STRefl) (coerce STRefl STRefl)) (STFnTy (STTrans CM MA) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STTrans (STFnTy AP STRefl) (coerce STRefl STRefl)) (STFnTy (STTrans CM MA) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (let* (((: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) (synthesize (: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) kb rb (S (S Z))))) (: (STTrans (STTrans (coerce STRefl STRefl) STRefl) $proof2#20647) (<: (-> Physical Weight) (-> Cat Weight)))), (let* (((: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) (synthesize (: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) kb rb (S (S Z))))) (: (STTrans (STTrans (coerce STRefl STRefl) (STTrans STRefl STRefl)) $proof2#20647) (<: (-> Physical Weight) (-> Cat Weight)))), (let* (((: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) (synthesize (: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) kb rb (S (S Z))))) (: (STTrans (STTrans (coerce STRefl STRefl) (STFnTy STRefl STRefl)) $proof2#20647) (<: (-> Physical Weight) (-> Cat Weight)))), (: (STTrans (STTrans (coerce STRefl STRefl) (STFnTy AP STRefl)) (STTrans (STFnTy MA STRefl) (STFnTy CM STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STTrans (coerce STRefl STRefl) (STFnTy AP STRefl)) (STFnTy (STTrans CM MA) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STTrans (coerce STRefl STRefl) (STFnTy AP STRefl)) (STFnTy (STTrans CM MA) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STTrans (coerce STRefl STRefl) (STFnTy AP STRefl)) (STFnTy (STTrans CM MA) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (let* (((: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) (synthesize (: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) kb rb (S (S Z))))) (: (STTrans (STTrans (coerce STRefl STRefl) (coerce STRefl STRefl)) $proof2#20647) (<: (-> Physical Weight) (-> Cat Weight)))), (let* (((: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) (synthesize (: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) kb rb (S (S Z))))) (: (STTrans (STFnTy STRefl STRefl) $proof2#20647) (<: (-> Physical Weight) (-> Cat Weight)))), (let* (((: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) (synthesize (: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) kb rb (S (S Z))))) (: (STTrans (STFnTy STRefl (STTrans STRefl STRefl)) $proof2#20647) (<: (-> Physical Weight) (-> Cat Weight)))), (let* (((: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) (synthesize (: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) kb rb (S (S Z))))) (: (STTrans (STFnTy STRefl (coerce STRefl STRefl)) $proof2#20647) (<: (-> Physical Weight) (-> Cat Weight)))), (: (STTrans (STFnTy AP STRefl) (STTrans (STFnTy MA STRefl) (STFnTy CM STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy AP STRefl) (STFnTy (STTrans CM MA) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy AP STRefl) (STFnTy (STTrans CM MA) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy AP STRefl) (STFnTy (STTrans CM MA) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy AP (STTrans STRefl STRefl)) (STTrans (STFnTy MA STRefl) (STFnTy CM STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy AP (STTrans STRefl STRefl)) (STFnTy (STTrans CM MA) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy AP (STTrans STRefl STRefl)) (STFnTy (STTrans CM MA) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy AP (STTrans STRefl STRefl)) (STFnTy (STTrans CM MA) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy AP (coerce STRefl STRefl)) (STTrans (STFnTy MA STRefl) (STFnTy CM STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy AP (coerce STRefl STRefl)) (STFnTy (STTrans CM MA) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy AP (coerce STRefl STRefl)) (STFnTy (STTrans CM MA) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy AP (coerce STRefl STRefl)) (STFnTy (STTrans CM MA) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (let* (((: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) (synthesize (: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) kb rb (S (S Z))))) (: (STTrans (STFnTy (STTrans STRefl STRefl) STRefl) $proof2#20647) (<: (-> Physical Weight) (-> Cat Weight)))), (let* (((: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) (synthesize (: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) kb rb (S (S Z))))) (: (STTrans (STFnTy (STTrans STRefl STRefl) (STTrans STRefl STRefl)) $proof2#20647) (<: (-> Physical Weight) (-> Cat Weight)))), (let* (((: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) (synthesize (: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) kb rb (S (S Z))))) (: (STTrans (STFnTy (STTrans STRefl STRefl) (coerce STRefl STRefl)) $proof2#20647) (<: (-> Physical Weight) (-> Cat Weight)))), (: (STTrans (STFnTy (STTrans STRefl AP) STRefl) (STTrans (STFnTy MA STRefl) (STFnTy CM STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans STRefl AP) STRefl) (STFnTy (STTrans CM MA) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans STRefl AP) STRefl) (STFnTy (STTrans CM MA) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans STRefl AP) STRefl) (STFnTy (STTrans CM MA) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans STRefl AP) (STTrans STRefl STRefl)) (STTrans (STFnTy MA STRefl) (STFnTy CM STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans STRefl AP) (STTrans STRefl STRefl)) (STFnTy (STTrans CM MA) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans STRefl AP) (STTrans STRefl STRefl)) (STFnTy (STTrans CM MA) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans STRefl AP) (STTrans STRefl STRefl)) (STFnTy (STTrans CM MA) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans STRefl AP) (coerce STRefl STRefl)) (STTrans (STFnTy MA STRefl) (STFnTy CM STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans STRefl AP) (coerce STRefl STRefl)) (STFnTy (STTrans CM MA) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans STRefl AP) (coerce STRefl STRefl)) (STFnTy (STTrans CM MA) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans STRefl AP) (coerce STRefl STRefl)) (STFnTy (STTrans CM MA) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) STRefl) (STTrans STRefl (STFnTy CM STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) STRefl) (STTrans (STTrans STRefl STRefl) (STFnTy CM STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) STRefl) (STTrans (STFnTy STRefl STRefl) (STFnTy CM STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) STRefl) (STTrans (STFnTy CM STRefl) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) STRefl) (STTrans (STFnTy CM STRefl) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) STRefl) (STTrans (STFnTy CM STRefl) (STFnTy STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) STRefl) (STTrans (STFnTy CM STRefl) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) STRefl) (STTrans (coerce STRefl STRefl) (STFnTy CM STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) STRefl) (STFnTy CM STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) STRefl) (STFnTy CM (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) STRefl) (STFnTy CM (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) STRefl) (STFnTy (STTrans STRefl CM) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) STRefl) (STFnTy (STTrans STRefl CM) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) STRefl) (STFnTy (STTrans STRefl CM) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) STRefl) (STFnTy (STTrans CM STRefl) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) STRefl) (STFnTy (STTrans CM STRefl) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) STRefl) (STFnTy (STTrans CM STRefl) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) STRefl) (STFnTy (coerce STRefl CM) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) STRefl) (STFnTy (coerce STRefl CM) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) STRefl) (STFnTy (coerce STRefl CM) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) STRefl) (coerce STRefl (STFnTy CM STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) STRefl) (coerce (STTrans STRefl STRefl) (STFnTy CM STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) STRefl) (coerce (coerce STRefl STRefl) (STFnTy CM STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) (STTrans STRefl STRefl)) (STTrans STRefl (STFnTy CM STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) (STTrans STRefl STRefl)) (STTrans (STTrans STRefl STRefl) (STFnTy CM STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) (STTrans STRefl STRefl)) (STTrans (STFnTy STRefl STRefl) (STFnTy CM STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) (STTrans STRefl STRefl)) (STTrans (STFnTy CM STRefl) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) (STTrans STRefl STRefl)) (STTrans (STFnTy CM STRefl) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) (STTrans STRefl STRefl)) (STTrans (STFnTy CM STRefl) (STFnTy STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) (STTrans STRefl STRefl)) (STTrans (STFnTy CM STRefl) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) (STTrans STRefl STRefl)) (STTrans (coerce STRefl STRefl) (STFnTy CM STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) (STTrans STRefl STRefl)) (STFnTy CM STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) (STTrans STRefl STRefl)) (STFnTy CM (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) (STTrans STRefl STRefl)) (STFnTy CM (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) (STTrans STRefl STRefl)) (STFnTy (STTrans STRefl CM) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) (STTrans STRefl STRefl)) (STFnTy (STTrans STRefl CM) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) (STTrans STRefl STRefl)) (STFnTy (STTrans STRefl CM) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) (STTrans STRefl STRefl)) (STFnTy (STTrans CM STRefl) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) (STTrans STRefl STRefl)) (STFnTy (STTrans CM STRefl) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) (STTrans STRefl STRefl)) (STFnTy (STTrans CM STRefl) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) (STTrans STRefl STRefl)) (STFnTy (coerce STRefl CM) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) (STTrans STRefl STRefl)) (STFnTy (coerce STRefl CM) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) (STTrans STRefl STRefl)) (STFnTy (coerce STRefl CM) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) (STTrans STRefl STRefl)) (coerce STRefl (STFnTy CM STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) (STTrans STRefl STRefl)) (coerce (STTrans STRefl STRefl) (STFnTy CM STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) (STTrans STRefl STRefl)) (coerce (coerce STRefl STRefl) (STFnTy CM STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) (coerce STRefl STRefl)) (STTrans STRefl (STFnTy CM STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) (coerce STRefl STRefl)) (STTrans (STTrans STRefl STRefl) (STFnTy CM STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) (coerce STRefl STRefl)) (STTrans (STFnTy STRefl STRefl) (STFnTy CM STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) (coerce STRefl STRefl)) (STTrans (STFnTy CM STRefl) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) (coerce STRefl STRefl)) (STTrans (STFnTy CM STRefl) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) (coerce STRefl STRefl)) (STTrans (STFnTy CM STRefl) (STFnTy STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) (coerce STRefl STRefl)) (STTrans (STFnTy CM STRefl) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) (coerce STRefl STRefl)) (STTrans (coerce STRefl STRefl) (STFnTy CM STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) (coerce STRefl STRefl)) (STFnTy CM STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) (coerce STRefl STRefl)) (STFnTy CM (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) (coerce STRefl STRefl)) (STFnTy CM (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) (coerce STRefl STRefl)) (STFnTy (STTrans STRefl CM) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) (coerce STRefl STRefl)) (STFnTy (STTrans STRefl CM) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) (coerce STRefl STRefl)) (STFnTy (STTrans STRefl CM) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) (coerce STRefl STRefl)) (STFnTy (STTrans CM STRefl) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) (coerce STRefl STRefl)) (STFnTy (STTrans CM STRefl) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) (coerce STRefl STRefl)) (STFnTy (STTrans CM STRefl) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) (coerce STRefl STRefl)) (STFnTy (coerce STRefl CM) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) (coerce STRefl STRefl)) (STFnTy (coerce STRefl CM) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) (coerce STRefl STRefl)) (STFnTy (coerce STRefl CM) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) (coerce STRefl STRefl)) (coerce STRefl (STFnTy CM STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) (coerce STRefl STRefl)) (coerce (STTrans STRefl STRefl) (STFnTy CM STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans MA AP) (coerce STRefl STRefl)) (coerce (coerce STRefl STRefl) (STFnTy CM STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans AP STRefl) STRefl) (STTrans (STFnTy MA STRefl) (STFnTy CM STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans AP STRefl) STRefl) (STFnTy (STTrans CM MA) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans AP STRefl) STRefl) (STFnTy (STTrans CM MA) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans AP STRefl) STRefl) (STFnTy (STTrans CM MA) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans AP STRefl) (STTrans STRefl STRefl)) (STTrans (STFnTy MA STRefl) (STFnTy CM STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans AP STRefl) (STTrans STRefl STRefl)) (STFnTy (STTrans CM MA) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans AP STRefl) (STTrans STRefl STRefl)) (STFnTy (STTrans CM MA) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans AP STRefl) (STTrans STRefl STRefl)) (STFnTy (STTrans CM MA) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans AP STRefl) (coerce STRefl STRefl)) (STTrans (STFnTy MA STRefl) (STFnTy CM STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans AP STRefl) (coerce STRefl STRefl)) (STFnTy (STTrans CM MA) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans AP STRefl) (coerce STRefl STRefl)) (STFnTy (STTrans CM MA) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (STTrans AP STRefl) (coerce STRefl STRefl)) (STFnTy (STTrans CM MA) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (let* (((: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) (synthesize (: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) kb rb (S (S Z))))) (: (STTrans (STFnTy (coerce STRefl STRefl) STRefl) $proof2#20647) (<: (-> Physical Weight) (-> Cat Weight)))), (let* (((: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) (synthesize (: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) kb rb (S (S Z))))) (: (STTrans (STFnTy (coerce STRefl STRefl) (STTrans STRefl STRefl)) $proof2#20647) (<: (-> Physical Weight) (-> Cat Weight)))), (let* (((: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) (synthesize (: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) kb rb (S (S Z))))) (: (STTrans (STFnTy (coerce STRefl STRefl) (coerce STRefl STRefl)) $proof2#20647) (<: (-> Physical Weight) (-> Cat Weight)))), (: (STTrans (STFnTy (coerce STRefl AP) STRefl) (STTrans (STFnTy MA STRefl) (STFnTy CM STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (coerce STRefl AP) STRefl) (STFnTy (STTrans CM MA) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (coerce STRefl AP) STRefl) (STFnTy (STTrans CM MA) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (coerce STRefl AP) STRefl) (STFnTy (STTrans CM MA) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (coerce STRefl AP) (STTrans STRefl STRefl)) (STTrans (STFnTy MA STRefl) (STFnTy CM STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (coerce STRefl AP) (STTrans STRefl STRefl)) (STFnTy (STTrans CM MA) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (coerce STRefl AP) (STTrans STRefl STRefl)) (STFnTy (STTrans CM MA) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (coerce STRefl AP) (STTrans STRefl STRefl)) (STFnTy (STTrans CM MA) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (coerce STRefl AP) (coerce STRefl STRefl)) (STTrans (STFnTy MA STRefl) (STFnTy CM STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (coerce STRefl AP) (coerce STRefl STRefl)) (STFnTy (STTrans CM MA) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (coerce STRefl AP) (coerce STRefl STRefl)) (STFnTy (STTrans CM MA) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (STFnTy (coerce STRefl AP) (coerce STRefl STRefl)) (STFnTy (STTrans CM MA) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (let* (((: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) (synthesize (: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) kb rb (S (S Z))))) (: (STTrans (coerce STRefl STRefl) $proof2#20647) (<: (-> Physical Weight) (-> Cat Weight)))), (let* (((: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) (synthesize (: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) kb rb (S (S Z))))) (: (STTrans (coerce STRefl (STTrans STRefl STRefl)) $proof2#20647) (<: (-> Physical Weight) (-> Cat Weight)))), (let* (((: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) (synthesize (: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) kb rb (S (S Z))))) (: (STTrans (coerce STRefl (STFnTy STRefl STRefl)) $proof2#20647) (<: (-> Physical Weight) (-> Cat Weight)))), (: (STTrans (coerce STRefl (STFnTy AP STRefl)) (STTrans (STFnTy MA STRefl) (STFnTy CM STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (coerce STRefl (STFnTy AP STRefl)) (STFnTy (STTrans CM MA) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (coerce STRefl (STFnTy AP STRefl)) (STFnTy (STTrans CM MA) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (coerce STRefl (STFnTy AP STRefl)) (STFnTy (STTrans CM MA) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (let* (((: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) (synthesize (: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) kb rb (S (S Z))))) (: (STTrans (coerce STRefl (coerce STRefl STRefl)) $proof2#20647) (<: (-> Physical Weight) (-> Cat Weight)))), (let* (((: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) (synthesize (: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) kb rb (S (S Z))))) (: (STTrans (coerce (STTrans STRefl STRefl) STRefl) $proof2#20647) (<: (-> Physical Weight) (-> Cat Weight)))), (let* (((: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) (synthesize (: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) kb rb (S (S Z))))) (: (STTrans (coerce (STTrans STRefl STRefl) (STTrans STRefl STRefl)) $proof2#20647) (<: (-> Physical Weight) (-> Cat Weight)))), (let* (((: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) (synthesize (: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) kb rb (S (S Z))))) (: (STTrans (coerce (STTrans STRefl STRefl) (STFnTy STRefl STRefl)) $proof2#20647) (<: (-> Physical Weight) (-> Cat Weight)))), (: (STTrans (coerce (STTrans STRefl STRefl) (STFnTy AP STRefl)) (STTrans (STFnTy MA STRefl) (STFnTy CM STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (coerce (STTrans STRefl STRefl) (STFnTy AP STRefl)) (STFnTy (STTrans CM MA) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (coerce (STTrans STRefl STRefl) (STFnTy AP STRefl)) (STFnTy (STTrans CM MA) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (coerce (STTrans STRefl STRefl) (STFnTy AP STRefl)) (STFnTy (STTrans CM MA) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (let* (((: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) (synthesize (: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) kb rb (S (S Z))))) (: (STTrans (coerce (STTrans STRefl STRefl) (coerce STRefl STRefl)) $proof2#20647) (<: (-> Physical Weight) (-> Cat Weight)))), (let* (((: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) (synthesize (: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) kb rb (S (S Z))))) (: (STTrans (coerce (coerce STRefl STRefl) STRefl) $proof2#20647) (<: (-> Physical Weight) (-> Cat Weight)))), (let* (((: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) (synthesize (: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) kb rb (S (S Z))))) (: (STTrans (coerce (coerce STRefl STRefl) (STTrans STRefl STRefl)) $proof2#20647) (<: (-> Physical Weight) (-> Cat Weight)))), (let* (((: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) (synthesize (: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) kb rb (S (S Z))))) (: (STTrans (coerce (coerce STRefl STRefl) (STFnTy STRefl STRefl)) $proof2#20647) (<: (-> Physical Weight) (-> Cat Weight)))), (: (STTrans (coerce (coerce STRefl STRefl) (STFnTy AP STRefl)) (STTrans (STFnTy MA STRefl) (STFnTy CM STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (coerce (coerce STRefl STRefl) (STFnTy AP STRefl)) (STFnTy (STTrans CM MA) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (coerce (coerce STRefl STRefl) (STFnTy AP STRefl)) (STFnTy (STTrans CM MA) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STTrans (coerce (coerce STRefl STRefl) (STFnTy AP STRefl)) (STFnTy (STTrans CM MA) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (let* (((: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) (synthesize (: $proof2#20647 (<: (-> Physical Weight) (-> Cat Weight))) kb rb (S (S Z))))) (: (STTrans (coerce (coerce STRefl STRefl) (coerce STRefl STRefl)) $proof2#20647) (<: (-> Physical Weight) (-> Cat Weight)))), (: (STFnTy (STTrans CM (STTrans MA AP)) STRefl) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans CM (STTrans MA AP)) (STTrans STRefl STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans CM (STTrans MA AP)) (STTrans STRefl (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans CM (STTrans MA AP)) (STTrans STRefl (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans CM (STTrans MA AP)) (STTrans (STTrans STRefl STRefl) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans CM (STTrans MA AP)) (STTrans (STTrans STRefl STRefl) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans CM (STTrans MA AP)) (STTrans (STTrans STRefl STRefl) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans CM (STTrans MA AP)) (STTrans (coerce STRefl STRefl) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans CM (STTrans MA AP)) (STTrans (coerce STRefl STRefl) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans CM (STTrans MA AP)) (STTrans (coerce STRefl STRefl) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans CM (STTrans MA AP)) (coerce STRefl STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans CM (STTrans MA AP)) (coerce STRefl (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans CM (STTrans MA AP)) (coerce STRefl (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans CM (STTrans MA AP)) (coerce (STTrans STRefl STRefl) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans CM (STTrans MA AP)) (coerce (STTrans STRefl STRefl) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans CM (STTrans MA AP)) (coerce (STTrans STRefl STRefl) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans CM (STTrans MA AP)) (coerce (coerce STRefl STRefl) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans CM (STTrans MA AP)) (coerce (coerce STRefl STRefl) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans CM (STTrans MA AP)) (coerce (coerce STRefl STRefl) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans STRefl CM) (STTrans MA AP)) STRefl) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans STRefl CM) (STTrans MA AP)) (STTrans STRefl STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans STRefl CM) (STTrans MA AP)) (STTrans STRefl (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans STRefl CM) (STTrans MA AP)) (STTrans STRefl (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans STRefl CM) (STTrans MA AP)) (STTrans (STTrans STRefl STRefl) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans STRefl CM) (STTrans MA AP)) (STTrans (STTrans STRefl STRefl) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans STRefl CM) (STTrans MA AP)) (STTrans (STTrans STRefl STRefl) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans STRefl CM) (STTrans MA AP)) (STTrans (coerce STRefl STRefl) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans STRefl CM) (STTrans MA AP)) (STTrans (coerce STRefl STRefl) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans STRefl CM) (STTrans MA AP)) (STTrans (coerce STRefl STRefl) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans STRefl CM) (STTrans MA AP)) (coerce STRefl STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans STRefl CM) (STTrans MA AP)) (coerce STRefl (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans STRefl CM) (STTrans MA AP)) (coerce STRefl (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans STRefl CM) (STTrans MA AP)) (coerce (STTrans STRefl STRefl) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans STRefl CM) (STTrans MA AP)) (coerce (STTrans STRefl STRefl) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans STRefl CM) (STTrans MA AP)) (coerce (STTrans STRefl STRefl) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans STRefl CM) (STTrans MA AP)) (coerce (coerce STRefl STRefl) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans STRefl CM) (STTrans MA AP)) (coerce (coerce STRefl STRefl) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans STRefl CM) (STTrans MA AP)) (coerce (coerce STRefl STRefl) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM STRefl) (STTrans MA AP)) STRefl) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM STRefl) (STTrans MA AP)) (STTrans STRefl STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM STRefl) (STTrans MA AP)) (STTrans STRefl (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM STRefl) (STTrans MA AP)) (STTrans STRefl (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM STRefl) (STTrans MA AP)) (STTrans (STTrans STRefl STRefl) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM STRefl) (STTrans MA AP)) (STTrans (STTrans STRefl STRefl) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM STRefl) (STTrans MA AP)) (STTrans (STTrans STRefl STRefl) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM STRefl) (STTrans MA AP)) (STTrans (coerce STRefl STRefl) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM STRefl) (STTrans MA AP)) (STTrans (coerce STRefl STRefl) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM STRefl) (STTrans MA AP)) (STTrans (coerce STRefl STRefl) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM STRefl) (STTrans MA AP)) (coerce STRefl STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM STRefl) (STTrans MA AP)) (coerce STRefl (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM STRefl) (STTrans MA AP)) (coerce STRefl (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM STRefl) (STTrans MA AP)) (coerce (STTrans STRefl STRefl) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM STRefl) (STTrans MA AP)) (coerce (STTrans STRefl STRefl) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM STRefl) (STTrans MA AP)) (coerce (STTrans STRefl STRefl) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM STRefl) (STTrans MA AP)) (coerce (coerce STRefl STRefl) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM STRefl) (STTrans MA AP)) (coerce (coerce STRefl STRefl) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM STRefl) (STTrans MA AP)) (coerce (coerce STRefl STRefl) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) AP) STRefl) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) AP) (STTrans STRefl STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) AP) (STTrans STRefl (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) AP) (STTrans STRefl (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) AP) (STTrans (STTrans STRefl STRefl) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) AP) (STTrans (STTrans STRefl STRefl) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) AP) (STTrans (STTrans STRefl STRefl) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) AP) (STTrans (coerce STRefl STRefl) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) AP) (STTrans (coerce STRefl STRefl) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) AP) (STTrans (coerce STRefl STRefl) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) AP) (coerce STRefl STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) AP) (coerce STRefl (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) AP) (coerce STRefl (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) AP) (coerce (STTrans STRefl STRefl) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) AP) (coerce (STTrans STRefl STRefl) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) AP) (coerce (STTrans STRefl STRefl) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) AP) (coerce (coerce STRefl STRefl) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) AP) (coerce (coerce STRefl STRefl) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) AP) (coerce (coerce STRefl STRefl) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) (STTrans STRefl AP)) STRefl) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) (STTrans STRefl AP)) (STTrans STRefl STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) (STTrans STRefl AP)) (STTrans STRefl (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) (STTrans STRefl AP)) (STTrans STRefl (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) (STTrans STRefl AP)) (STTrans (STTrans STRefl STRefl) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) (STTrans STRefl AP)) (STTrans (STTrans STRefl STRefl) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) (STTrans STRefl AP)) (STTrans (STTrans STRefl STRefl) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) (STTrans STRefl AP)) (STTrans (coerce STRefl STRefl) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) (STTrans STRefl AP)) (STTrans (coerce STRefl STRefl) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) (STTrans STRefl AP)) (STTrans (coerce STRefl STRefl) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) (STTrans STRefl AP)) (coerce STRefl STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) (STTrans STRefl AP)) (coerce STRefl (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) (STTrans STRefl AP)) (coerce STRefl (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) (STTrans STRefl AP)) (coerce (STTrans STRefl STRefl) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) (STTrans STRefl AP)) (coerce (STTrans STRefl STRefl) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) (STTrans STRefl AP)) (coerce (STTrans STRefl STRefl) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) (STTrans STRefl AP)) (coerce (coerce STRefl STRefl) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) (STTrans STRefl AP)) (coerce (coerce STRefl STRefl) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) (STTrans STRefl AP)) (coerce (coerce STRefl STRefl) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) (STTrans AP STRefl)) STRefl) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) (STTrans AP STRefl)) (STTrans STRefl STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) (STTrans AP STRefl)) (STTrans STRefl (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) (STTrans AP STRefl)) (STTrans STRefl (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) (STTrans AP STRefl)) (STTrans (STTrans STRefl STRefl) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) (STTrans AP STRefl)) (STTrans (STTrans STRefl STRefl) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) (STTrans AP STRefl)) (STTrans (STTrans STRefl STRefl) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) (STTrans AP STRefl)) (STTrans (coerce STRefl STRefl) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) (STTrans AP STRefl)) (STTrans (coerce STRefl STRefl) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) (STTrans AP STRefl)) (STTrans (coerce STRefl STRefl) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) (STTrans AP STRefl)) (coerce STRefl STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) (STTrans AP STRefl)) (coerce STRefl (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) (STTrans AP STRefl)) (coerce STRefl (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) (STTrans AP STRefl)) (coerce (STTrans STRefl STRefl) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) (STTrans AP STRefl)) (coerce (STTrans STRefl STRefl) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) (STTrans AP STRefl)) (coerce (STTrans STRefl STRefl) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) (STTrans AP STRefl)) (coerce (coerce STRefl STRefl) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) (STTrans AP STRefl)) (coerce (coerce STRefl STRefl) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) (STTrans AP STRefl)) (coerce (coerce STRefl STRefl) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) (coerce STRefl AP)) STRefl) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) (coerce STRefl AP)) (STTrans STRefl STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) (coerce STRefl AP)) (STTrans STRefl (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) (coerce STRefl AP)) (STTrans STRefl (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) (coerce STRefl AP)) (STTrans (STTrans STRefl STRefl) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) (coerce STRefl AP)) (STTrans (STTrans STRefl STRefl) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) (coerce STRefl AP)) (STTrans (STTrans STRefl STRefl) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) (coerce STRefl AP)) (STTrans (coerce STRefl STRefl) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) (coerce STRefl AP)) (STTrans (coerce STRefl STRefl) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) (coerce STRefl AP)) (STTrans (coerce STRefl STRefl) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) (coerce STRefl AP)) (coerce STRefl STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) (coerce STRefl AP)) (coerce STRefl (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) (coerce STRefl AP)) (coerce STRefl (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) (coerce STRefl AP)) (coerce (STTrans STRefl STRefl) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) (coerce STRefl AP)) (coerce (STTrans STRefl STRefl) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) (coerce STRefl AP)) (coerce (STTrans STRefl STRefl) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) (coerce STRefl AP)) (coerce (coerce STRefl STRefl) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) (coerce STRefl AP)) (coerce (coerce STRefl STRefl) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (STTrans CM MA) (coerce STRefl AP)) (coerce (coerce STRefl STRefl) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (coerce STRefl CM) (STTrans MA AP)) STRefl) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (coerce STRefl CM) (STTrans MA AP)) (STTrans STRefl STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (coerce STRefl CM) (STTrans MA AP)) (STTrans STRefl (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (coerce STRefl CM) (STTrans MA AP)) (STTrans STRefl (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (coerce STRefl CM) (STTrans MA AP)) (STTrans (STTrans STRefl STRefl) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (coerce STRefl CM) (STTrans MA AP)) (STTrans (STTrans STRefl STRefl) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (coerce STRefl CM) (STTrans MA AP)) (STTrans (STTrans STRefl STRefl) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (coerce STRefl CM) (STTrans MA AP)) (STTrans (coerce STRefl STRefl) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (coerce STRefl CM) (STTrans MA AP)) (STTrans (coerce STRefl STRefl) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (coerce STRefl CM) (STTrans MA AP)) (STTrans (coerce STRefl STRefl) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (coerce STRefl CM) (STTrans MA AP)) (coerce STRefl STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (coerce STRefl CM) (STTrans MA AP)) (coerce STRefl (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (coerce STRefl CM) (STTrans MA AP)) (coerce STRefl (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (coerce STRefl CM) (STTrans MA AP)) (coerce (STTrans STRefl STRefl) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (coerce STRefl CM) (STTrans MA AP)) (coerce (STTrans STRefl STRefl) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (coerce STRefl CM) (STTrans MA AP)) (coerce (STTrans STRefl STRefl) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (coerce STRefl CM) (STTrans MA AP)) (coerce (coerce STRefl STRefl) STRefl)) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (coerce STRefl CM) (STTrans MA AP)) (coerce (coerce STRefl STRefl) (STTrans STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (: (STFnTy (STTrans (coerce STRefl CM) (STTrans MA AP)) (coerce (coerce STRefl STRefl) (coerce STRefl STRefl))) (<: (-> Physical Weight) (-> Cat Weight))), (let* (((: $proof2#128027 (<: (-> Physical Weight) (-> Cat Weight))) (synthesize (: $proof2#128027 (<: (-> Physical Weight) (-> Cat Weight))) kb rb (S (S Z))))) (: (coerce STRefl $proof2#128027) (<: (-> Physical Weight) (-> Cat Weight)))), (let* (((: $proof2#128027 (<: (-> Physical Weight) (-> Cat Weight))) (synthesize (: $proof2#128027 (<: (-> Physical Weight) (-> Cat Weight))) kb rb (S (S Z))))) (: (coerce (STTrans STRefl STRefl) $proof2#128027) (<: (-> Physical Weight) (-> Cat Weight)))), (let* (((: $proof2#128027 (<: (-> Physical Weight) (-> Cat Weight))) (synthesize (: $proof2#128027 (<: (-> Physical Weight) (-> Cat Weight))) kb rb (S (S Z))))) (: (coerce (STTrans STRefl (STTrans STRefl STRefl)) $proof2#128027) (<: (-> Physical Weight) (-> Cat Weight)))), (let* (((: $proof2#128027 (<: (-> Physical Weight) (-> Cat Weight))) (synthesize (: $proof2#128027 (<: (-> Physical Weight) (-> Cat Weight))) kb rb (S (S Z))))) (: (coerce (STTrans STRefl (coerce STRefl STRefl)) $proof2#128027) (<: (-> Physical Weight) (-> Cat Weight)))), (let* (((: $proof2#128027 (<: (-> Physical Weight) (-> Cat Weight))) (synthesize (: $proof2#128027 (<: (-> Physical Weight) (-> Cat Weight))) kb rb (S (S Z))))) (: (coerce (STTrans (STTrans STRefl STRefl) STRefl) $proof2#128027) (<: (-> Physical Weight) (-> Cat Weight)))), (let* (((: $proof2#128027 (<: (-> Physical Weight) (-> Cat Weight))) (synthesize (: $proof2#128027 (<: (-> Physical Weight) (-> Cat Weight))) kb rb (S (S Z))))) (: (coerce (STTrans (STTrans STRefl STRefl) (STTrans STRefl STRefl)) $proof2#128027) (<: (-> Physical Weight) (-> Cat Weight)))), (let* (((: $proof2#128027 (<: (-> Physical Weight) (-> Cat Weight))) (synthesize (: $proof2#128027 (<: (-> Physical Weight) (-> Cat Weight))) kb rb (S (S Z))))) (: (coerce (STTrans (STTrans STRefl STRefl) (coerce STRefl STRefl)) $proof2#128027) (<: (-> Physical Weight) (-> Cat Weight)))), (let* (((: $proof2#128027 (<: (-> Physical Weight) (-> Cat Weight))) (synthesize (: $proof2#128027 (<: (-> Physical Weight) (-> Cat Weight))) kb rb (S (S Z))))) (: (coerce (STTrans (coerce STRefl STRefl) STRefl) $proof2#128027) (<: (-> Physical Weight) (-> Cat Weight)))), (let* (((: $proof2#128027 (<: (-> Physical Weight) (-> Cat Weight))) (synthesize (: $proof2#128027 (<: (-> Physical Weight) (-> Cat Weight))) kb rb (S (S Z))))) (: (coerce (STTrans (coerce STRefl STRefl) (STTrans STRefl STRefl)) $proof2#128027) (<: (-> Physical Weight) (-> Cat Weight)))), (let* (((: $proof2#128027 (<: (-> Physical Weight) (-> Cat Weight))) (synthesize (: $proof2#128027 (<: (-> Physical Weight) (-> Cat Weight))) kb rb (S (S Z))))) (: (coerce (STTrans (coerce STRefl STRefl) (coerce STRefl STRefl)) $proof2#128027) (<: (-> Physical Weight) (-> Cat Weight)))), (let* (((: $proof2#128027 (<: (-> Physical Weight) (-> Cat Weight))) (synthesize (: $proof2#128027 (<: (-> Physical Weight) (-> Cat Weight))) kb rb (S (S Z))))) (: (coerce (coerce STRefl STRefl) $proof2#128027) (<: (-> Physical Weight) (-> Cat Weight)))), (let* (((: $proof2#128027 (<: (-> Physical Weight) (-> Cat Weight))) (synthesize (: $proof2#128027 (<: (-> Physical Weight) (-> Cat Weight))) kb rb (S (S Z))))) (: (coerce (coerce STRefl (STTrans STRefl STRefl)) $proof2#128027) (<: (-> Physical Weight) (-> Cat Weight)))), (let* (((: $proof2#128027 (<: (-> Physical Weight) (-> Cat Weight))) (synthesize (: $proof2#128027 (<: (-> Physical Weight) (-> Cat Weight))) kb rb (S (S Z))))) (: (coerce (coerce STRefl (coerce STRefl STRefl)) $proof2#128027) (<: (-> Physical Weight) (-> Cat Weight)))), (let* (((: $proof2#128027 (<: (-> Physical Weight) (-> Cat Weight))) (synthesize (: $proof2#128027 (<: (-> Physical Weight) (-> Cat Weight))) kb rb (S (S Z))))) (: (coerce (coerce (STTrans STRefl STRefl) STRefl) $proof2#128027) (<: (-> Physical Weight) (-> Cat Weight)))), (let* (((: $proof2#128027 (<: (-> Physical Weight) (-> Cat Weight))) (synthesize (: $proof2#128027 (<: (-> Physical Weight) (-> Cat Weight))) kb rb (S (S Z))))) (: (coerce (coerce (STTrans STRefl STRefl) (STTrans STRefl STRefl)) $proof2#128027) (<: (-> Physical Weight) (-> Cat Weight)))), (let* (((: $proof2#128027 (<: (-> Physical Weight) (-> Cat Weight))) (synthesize (: $proof2#128027 (<: (-> Physical Weight) (-> Cat Weight))) kb rb (S (S Z))))) (: (coerce (coerce (STTrans STRefl STRefl) (coerce STRefl STRefl)) $proof2#128027) (<: (-> Physical Weight) (-> Cat Weight)))), (let* (((: $proof2#128027 (<: (-> Physical Weight) (-> Cat Weight))) (synthesize (: $proof2#128027 (<: (-> Physical Weight) (-> Cat Weight))) kb rb (S (S Z))))) (: (coerce (coerce (coerce STRefl STRefl) STRefl) $proof2#128027) (<: (-> Physical Weight) (-> Cat Weight)))), (let* (((: $proof2#128027 (<: (-> Physical Weight) (-> Cat Weight))) (synthesize (: $proof2#128027 (<: (-> Physical Weight) (-> Cat Weight))) kb rb (S (S Z))))) (: (coerce (coerce (coerce STRefl STRefl) (STTrans STRefl STRefl)) $proof2#128027) (<: (-> Physical Weight) (-> Cat Weight)))), (let* (((: $proof2#128027 (<: (-> Physical Weight) (-> Cat Weight))) (synthesize (: $proof2#128027 (<: (-> Physical Weight) (-> Cat Weight))) kb rb (S (S Z))))) (: (coerce (coerce (coerce STRefl STRefl) (coerce STRefl STRefl)) $proof2#128027) (<: (-> Physical Weight) (-> Cat Weight))))]
[(: weigh (-> Physical Weight))]
[(: wPW (: weigh (-> Physical Weight)))]
[(let* (((: $proof2#185969 (-> Cat Weight)) (synthesize (: $proof2#185969 (-> Cat Weight)) kb rb (S (S Z))))) (: (coerce STRefl $proof2#185969) (-> Cat Weight))), (let* (((: $proof2#185969 (-> Cat Weight)) (synthesize (: $proof2#185969 (-> Cat Weight)) kb rb (S (S Z))))) (: (coerce (STTrans STRefl STRefl) $proof2#185969) (-> Cat Weight))), (let* (((: $proof2#185969 (-> Cat Weight)) (synthesize (: $proof2#185969 (-> Cat Weight)) kb rb (S (S Z))))) (: (coerce (STTrans STRefl (STTrans STRefl STRefl)) $proof2#185969) (-> Cat Weight))), (let* (((: $proof2#185969 (-> Cat Weight)) (synthesize (: $proof2#185969 (-> Cat Weight)) kb rb (S (S Z))))) (: (coerce (STTrans STRefl (STFnTy STRefl STRefl)) $proof2#185969) (-> Cat Weight))), (let* (((: $proof2#185969 (-> Mammal Weight)) (synthesize (: $proof2#185969 (-> Mammal Weight)) kb rb (S (S Z))))) (: (coerce (STTrans STRefl (STFnTy CM STRefl)) $proof2#185969) (-> Cat Weight))), (let* (((: $proof2#185969 (-> Cat Weight)) (synthesize (: $proof2#185969 (-> Cat Weight)) kb rb (S (S Z))))) (: (coerce (STTrans STRefl (coerce STRefl STRefl)) $proof2#185969) (-> Cat Weight))), (let* (((: $proof2#185969 (-> Cat Weight)) (synthesize (: $proof2#185969 (-> Cat Weight)) kb rb (S (S Z))))) (: (coerce (STTrans (STTrans STRefl STRefl) STRefl) $proof2#185969) (-> Cat Weight))), (let* (((: $proof2#185969 (-> Cat Weight)) (synthesize (: $proof2#185969 (-> Cat Weight)) kb rb (S (S Z))))) (: (coerce (STTrans (STTrans STRefl STRefl) (STTrans STRefl STRefl)) $proof2#185969) (-> Cat Weight))), (let* (((: $proof2#185969 (-> Cat Weight)) (synthesize (: $proof2#185969 (-> Cat Weight)) kb rb (S (S Z))))) (: (coerce (STTrans (STTrans STRefl STRefl) (STFnTy STRefl STRefl)) $proof2#185969) (-> Cat Weight))), (let* (((: $proof2#185969 (-> Mammal Weight)) (synthesize (: $proof2#185969 (-> Mammal Weight)) kb rb (S (S Z))))) (: (coerce (STTrans (STTrans STRefl STRefl) (STFnTy CM STRefl)) $proof2#185969) (-> Cat Weight))), (let* (((: $proof2#185969 (-> Cat Weight)) (synthesize (: $proof2#185969 (-> Cat Weight)) kb rb (S (S Z))))) (: (coerce (STTrans (STTrans STRefl STRefl) (coerce STRefl STRefl)) $proof2#185969) (-> Cat Weight))), (let* (((: $proof2#185969 (-> Cat Weight)) (synthesize (: $proof2#185969 (-> Cat Weight)) kb rb (S (S Z))))) (: (coerce (STTrans (STFnTy STRefl STRefl) STRefl) $proof2#185969) (-> Cat Weight))), (let* (((: $proof2#185969 (-> Cat Weight)) (synthesize (: $proof2#185969 (-> Cat Weight)) kb rb (S (S Z))))) (: (coerce (STTrans (STFnTy STRefl STRefl) (STTrans STRefl STRefl)) $proof2#185969) (-> Cat Weight))), (let* (((: $proof2#185969 (-> Cat Weight)) (synthesize (: $proof2#185969 (-> Cat Weight)) kb rb (S (S Z))))) (: (coerce (STTrans (STFnTy STRefl STRefl) (STFnTy STRefl STRefl)) $proof2#185969) (-> Cat Weight))), (let* (((: $proof2#185969 (-> Mammal Weight)) (synthesize (: $proof2#185969 (-> Mammal Weight)) kb rb (S (S Z))))) (: (coerce (STTrans (STFnTy STRefl STRefl) (STFnTy CM STRefl)) $proof2#185969) (-> Cat Weight))), (let* (((: $proof2#185969 (-> Cat Weight)) (synthesize (: $proof2#185969 (-> Cat Weight)) kb rb (S (S Z))))) (: (coerce (STTrans (STFnTy STRefl STRefl) (coerce STRefl STRefl)) $proof2#185969) (-> Cat Weight))), (let* (((: $proof2#185969 (-> Mammal Weight)) (synthesize (: $proof2#185969 (-> Mammal Weight)) kb rb (S (S Z))))) (: (coerce (STTrans (STFnTy CM STRefl) STRefl) $proof2#185969) (-> Cat Weight))), (let* (((: $proof2#185969 (-> Mammal Weight)) (synthesize (: $proof2#185969 (-> Mammal Weight)) kb rb (S (S Z))))) (: (coerce (STTrans (STFnTy CM STRefl) (STTrans STRefl STRefl)) $proof2#185969) (-> Cat Weight))), (let* (((: $proof2#185969 (-> Mammal Weight)) (synthesize (: $proof2#185969 (-> Mammal Weight)) kb rb (S (S Z))))) (: (coerce (STTrans (STFnTy CM STRefl) (STFnTy STRefl STRefl)) $proof2#185969) (-> Cat Weight))), (let* (((: $proof2#185969 (-> Mammal Weight)) (synthesize (: $proof2#185969 (-> Mammal Weight)) kb rb (S (S Z))))) (: (coerce (STTrans (STFnTy CM STRefl) (coerce STRefl STRefl)) $proof2#185969) (-> Cat Weight))), (: (coerce (STTrans (STFnTy MA STRefl) (STFnTy CM STRefl)) (coerce (STFnTy AP STRefl) weigh)) (-> Cat Weight)), (: (coerce (STTrans (STFnTy MA STRefl) (STFnTy CM STRefl)) (coerce (STFnTy AP STRefl) (coerce STRefl weigh))) (-> Cat Weight)), (let* (((: $proof2#185969 (-> Cat Weight)) (synthesize (: $proof2#185969 (-> Cat Weight)) kb rb (S (S Z))))) (: (coerce (STTrans (coerce STRefl STRefl) STRefl) $proof2#185969) (-> Cat Weight))), (let* (((: $proof2#185969 (-> Cat Weight)) (synthesize (: $proof2#185969 (-> Cat Weight)) kb rb (S (S Z))))) (: (coerce (STTrans (coerce STRefl STRefl) (STTrans STRefl STRefl)) $proof2#185969) (-> Cat Weight))), (let* (((: $proof2#185969 (-> Cat Weight)) (synthesize (: $proof2#185969 (-> Cat Weight)) kb rb (S (S Z))))) (: (coerce (STTrans (coerce STRefl STRefl) (STFnTy STRefl STRefl)) $proof2#185969) (-> Cat Weight))), (let* (((: $proof2#185969 (-> Mammal Weight)) (synthesize (: $proof2#185969 (-> Mammal Weight)) kb rb (S (S Z))))) (: (coerce (STTrans (coerce STRefl STRefl) (STFnTy CM STRefl)) $proof2#185969) (-> Cat Weight))), (let* (((: $proof2#185969 (-> Cat Weight)) (synthesize (: $proof2#185969 (-> Cat Weight)) kb rb (S (S Z))))) (: (coerce (STTrans (coerce STRefl STRefl) (coerce STRefl STRefl)) $proof2#185969) (-> Cat Weight))), (let* (((: $proof2#185969 (-> Cat Weight)) (synthesize (: $proof2#185969 (-> Cat Weight)) kb rb (S (S Z))))) (: (coerce (STFnTy STRefl STRefl) $proof2#185969) (-> Cat Weight))), (let* (((: $proof2#185969 (-> Cat Weight)) (synthesize (: $proof2#185969 (-> Cat Weight)) kb rb (S (S Z))))) (: (coerce (STFnTy STRefl (STTrans STRefl STRefl)) $proof2#185969) (-> Cat Weight))), (let* (((: $proof2#185969 (-> Cat Weight)) (synthesize (: $proof2#185969 (-> Cat Weight)) kb rb (S (S Z))))) (: (coerce (STFnTy STRefl (coerce STRefl STRefl)) $proof2#185969) (-> Cat Weight))), (let* (((: $proof2#185969 (-> Mammal Weight)) (synthesize (: $proof2#185969 (-> Mammal Weight)) kb rb (S (S Z))))) (: (coerce (STFnTy CM STRefl) $proof2#185969) (-> Cat Weight))), (let* (((: $proof2#185969 (-> Mammal Weight)) (synthesize (: $proof2#185969 (-> Mammal Weight)) kb rb (S (S Z))))) (: (coerce (STFnTy CM (STTrans STRefl STRefl)) $proof2#185969) (-> Cat Weight))), (let* (((: $proof2#185969 (-> Mammal Weight)) (synthesize (: $proof2#185969 (-> Mammal Weight)) kb rb (S (S Z))))) (: (coerce (STFnTy CM (coerce STRefl STRefl)) $proof2#185969) (-> Cat Weight))), (let* (((: $proof2#185969 (-> Cat Weight)) (synthesize (: $proof2#185969 (-> Cat Weight)) kb rb (S (S Z))))) (: (coerce (STFnTy (STTrans STRefl STRefl) STRefl) $proof2#185969) (-> Cat Weight))), (let* (((: $proof2#185969 (-> Cat Weight)) (synthesize (: $proof2#185969 (-> Cat Weight)) kb rb (S (S Z))))) (: (coerce (STFnTy (STTrans STRefl STRefl) (STTrans STRefl STRefl)) $proof2#185969) (-> Cat Weight))), (let* (((: $proof2#185969 (-> Cat Weight)) (synthesize (: $proof2#185969 (-> Cat Weight)) kb rb (S (S Z))))) (: (coerce (STFnTy (STTrans STRefl STRefl) (coerce STRefl STRefl)) $proof2#185969) (-> Cat Weight))), (let* (((: $proof2#185969 (-> Mammal Weight)) (synthesize (: $proof2#185969 (-> Mammal Weight)) kb rb (S (S Z))))) (: (coerce (STFnTy (STTrans STRefl CM) STRefl) $proof2#185969) (-> Cat Weight))), (let* (((: $proof2#185969 (-> Mammal Weight)) (synthesize (: $proof2#185969 (-> Mammal Weight)) kb rb (S (S Z))))) (: (coerce (STFnTy (STTrans STRefl CM) (STTrans STRefl STRefl)) $proof2#185969) (-> Cat Weight))), (let* (((: $proof2#185969 (-> Mammal Weight)) (synthesize (: $proof2#185969 (-> Mammal Weight)) kb rb (S (S Z))))) (: (coerce (STFnTy (STTrans STRefl CM) (coerce STRefl STRefl)) $proof2#185969) (-> Cat Weight))), (let* (((: $proof2#185969 (-> Mammal Weight)) (synthesize (: $proof2#185969 (-> Mammal Weight)) kb rb (S (S Z))))) (: (coerce (STFnTy (STTrans CM STRefl) STRefl) $proof2#185969) (-> Cat Weight))), (let* (((: $proof2#185969 (-> Mammal Weight)) (synthesize (: $proof2#185969 (-> Mammal Weight)) kb rb (S (S Z))))) (: (coerce (STFnTy (STTrans CM STRefl) (STTrans STRefl STRefl)) $proof2#185969) (-> Cat Weight))), (let* (((: $proof2#185969 (-> Mammal Weight)) (synthesize (: $proof2#185969 (-> Mammal Weight)) kb rb (S (S Z))))) (: (coerce (STFnTy (STTrans CM STRefl) (coerce STRefl STRefl)) $proof2#185969) (-> Cat Weight))), (: (coerce (STFnTy (STTrans CM MA) STRefl) (coerce (STFnTy AP STRefl) weigh)) (-> Cat Weight)), (: (coerce (STFnTy (STTrans CM MA) STRefl) (coerce (STFnTy AP STRefl) (coerce STRefl weigh))) (-> Cat Weight)), (: (coerce (STFnTy (STTrans CM MA) (STTrans STRefl STRefl)) (coerce (STFnTy AP STRefl) weigh)) (-> Cat Weight)), (: (coerce (STFnTy (STTrans CM MA) (STTrans STRefl STRefl)) (coerce (STFnTy AP STRefl) (coerce STRefl weigh))) (-> Cat Weight)), (: (coerce (STFnTy (STTrans CM MA) (coerce STRefl STRefl)) (coerce (STFnTy AP STRefl) weigh)) (-> Cat Weight)), (: (coerce (STFnTy (STTrans CM MA) (coerce STRefl STRefl)) (coerce (STFnTy AP STRefl) (coerce STRefl weigh))) (-> Cat Weight)), (let* (((: $proof2#185969 (-> Cat Weight)) (synthesize (: $proof2#185969 (-> Cat Weight)) kb rb (S (S Z))))) (: (coerce (STFnTy (coerce STRefl STRefl) STRefl) $proof2#185969) (-> Cat Weight))), (let* (((: $proof2#185969 (-> Cat Weight)) (synthesize (: $proof2#185969 (-> Cat Weight)) kb rb (S (S Z))))) (: (coerce (STFnTy (coerce STRefl STRefl) (STTrans STRefl STRefl)) $proof2#185969) (-> Cat Weight))), (let* (((: $proof2#185969 (-> Cat Weight)) (synthesize (: $proof2#185969 (-> Cat Weight)) kb rb (S (S Z))))) (: (coerce (STFnTy (coerce STRefl STRefl) (coerce STRefl STRefl)) $proof2#185969) (-> Cat Weight))), (let* (((: $proof2#185969 (-> Mammal Weight)) (synthesize (: $proof2#185969 (-> Mammal Weight)) kb rb (S (S Z))))) (: (coerce (STFnTy (coerce STRefl CM) STRefl) $proof2#185969) (-> Cat Weight))), (let* (((: $proof2#185969 (-> Mammal Weight)) (synthesize (: $proof2#185969 (-> Mammal Weight)) kb rb (S (S Z))))) (: (coerce (STFnTy (coerce STRefl CM) (STTrans STRefl STRefl)) $proof2#185969) (-> Cat Weight))), (let* (((: $proof2#185969 (-> Mammal Weight)) (synthesize (: $proof2#185969 (-> Mammal Weight)) kb rb (S (S Z))))) (: (coerce (STFnTy (coerce STRefl CM) (coerce STRefl STRefl)) $proof2#185969) (-> Cat Weight))), (let* (((: $proof2#185969 (-> Cat Weight)) (synthesize (: $proof2#185969 (-> Cat Weight)) kb rb (S (S Z))))) (: (coerce (coerce STRefl STRefl) $proof2#185969) (-> Cat Weight))), (let* (((: $proof2#185969 (-> Cat Weight)) (synthesize (: $proof2#185969 (-> Cat Weight)) kb rb (S (S Z))))) (: (coerce (coerce STRefl (STTrans STRefl STRefl)) $proof2#185969) (-> Cat Weight))), (let* (((: $proof2#185969 (-> Cat Weight)) (synthesize (: $proof2#185969 (-> Cat Weight)) kb rb (S (S Z))))) (: (coerce (coerce STRefl (STFnTy STRefl STRefl)) $proof2#185969) (-> Cat Weight))), (let* (((: $proof2#185969 (-> Mammal Weight)) (synthesize (: $proof2#185969 (-> Mammal Weight)) kb rb (S (S Z))))) (: (coerce (coerce STRefl (STFnTy CM STRefl)) $proof2#185969) (-> Cat Weight))), (let* (((: $proof2#185969 (-> Cat Weight)) (synthesize (: $proof2#185969 (-> Cat Weight)) kb rb (S (S Z))))) (: (coerce (coerce STRefl (coerce STRefl STRefl)) $proof2#185969) (-> Cat Weight))), (let* (((: $proof2#185969 (-> Cat Weight)) (synthesize (: $proof2#185969 (-> Cat Weight)) kb rb (S (S Z))))) (: (coerce (coerce (STTrans STRefl STRefl) STRefl) $proof2#185969) (-> Cat Weight))), (let* (((: $proof2#185969 (-> Cat Weight)) (synthesize (: $proof2#185969 (-> Cat Weight)) kb rb (S (S Z))))) (: (coerce (coerce (STTrans STRefl STRefl) (STTrans STRefl STRefl)) $proof2#185969) (-> Cat Weight))), (let* (((: $proof2#185969 (-> Cat Weight)) (synthesize (: $proof2#185969 (-> Cat Weight)) kb rb (S (S Z))))) (: (coerce (coerce (STTrans STRefl STRefl) (STFnTy STRefl STRefl)) $proof2#185969) (-> Cat Weight))), (let* (((: $proof2#185969 (-> Mammal Weight)) (synthesize (: $proof2#185969 (-> Mammal Weight)) kb rb (S (S Z))))) (: (coerce (coerce (STTrans STRefl STRefl) (STFnTy CM STRefl)) $proof2#185969) (-> Cat Weight))), (let* (((: $proof2#185969 (-> Cat Weight)) (synthesize (: $proof2#185969 (-> Cat Weight)) kb rb (S (S Z))))) (: (coerce (coerce (STTrans STRefl STRefl) (coerce STRefl STRefl)) $proof2#185969) (-> Cat Weight))), (let* (((: $proof2#185969 (-> Cat Weight)) (synthesize (: $proof2#185969 (-> Cat Weight)) kb rb (S (S Z))))) (: (coerce (coerce (coerce STRefl STRefl) STRefl) $proof2#185969) (-> Cat Weight))), (let* (((: $proof2#185969 (-> Cat Weight)) (synthesize (: $proof2#185969 (-> Cat Weight)) kb rb (S (S Z))))) (: (coerce (coerce (coerce STRefl STRefl) (STTrans STRefl STRefl)) $proof2#185969) (-> Cat Weight))), (let* (((: $proof2#185969 (-> Cat Weight)) (synthesize (: $proof2#185969 (-> Cat Weight)) kb rb (S (S Z))))) (: (coerce (coerce (coerce STRefl STRefl) (STFnTy STRefl STRefl)) $proof2#185969) (-> Cat Weight))), (let* (((: $proof2#185969 (-> Mammal Weight)) (synthesize (: $proof2#185969 (-> Mammal Weight)) kb rb (S (S Z))))) (: (coerce (coerce (coerce STRefl STRefl) (STFnTy CM STRefl)) $proof2#185969) (-> Cat Weight))), (let* (((: $proof2#185969 (-> Cat Weight)) (synthesize (: $proof2#185969 (-> Cat Weight)) kb rb (S (S Z))))) (: (coerce (coerce (coerce STRefl STRefl) (coerce STRefl STRefl)) $proof2#185969) (-> Cat Weight)))]
[(let* (((: $proof2#254208 (: $fun (-> Cat Weight))) (synthesize (: $proof2#254208 (: $fun (-> Cat Weight))) kb rb (S (S Z))))) (: (STImplCoer STRefl $proof2#254208) (: $fun (-> Cat Weight)))), (let* (((: $proof2#254208 (: $fun (-> Cat Weight))) (synthesize (: $proof2#254208 (: $fun (-> Cat Weight))) kb rb (S (S Z))))) (: (STImplCoer (STTrans STRefl STRefl) $proof2#254208) (: $fun (-> Cat Weight)))), (let* (((: $proof2#254208 (: $fun (-> Cat Weight))) (synthesize (: $proof2#254208 (: $fun (-> Cat Weight))) kb rb (S (S Z))))) (: (STImplCoer (STTrans STRefl (STTrans STRefl STRefl)) $proof2#254208) (: $fun (-> Cat Weight)))), (let* (((: $proof2#254208 (: $fun (-> Cat Weight))) (synthesize (: $proof2#254208 (: $fun (-> Cat Weight))) kb rb (S (S Z))))) (: (STImplCoer (STTrans STRefl (STFnTy STRefl STRefl)) $proof2#254208) (: $fun (-> Cat Weight)))), (let* (((: $proof2#254208 (: $fun (-> Mammal Weight))) (synthesize (: $proof2#254208 (: $fun (-> Mammal Weight))) kb rb (S (S Z))))) (: (STImplCoer (STTrans STRefl (STFnTy CM STRefl)) $proof2#254208) (: $fun (-> Cat Weight)))), (let* (((: $proof2#254208 (: $fun (-> Cat Weight))) (synthesize (: $proof2#254208 (: $fun (-> Cat Weight))) kb rb (S (S Z))))) (: (STImplCoer (STTrans STRefl (coerce STRefl STRefl)) $proof2#254208) (: $fun (-> Cat Weight)))), (let* (((: $proof2#254208 (: $fun (-> Cat Weight))) (synthesize (: $proof2#254208 (: $fun (-> Cat Weight))) kb rb (S (S Z))))) (: (STImplCoer (STTrans (STTrans STRefl STRefl) STRefl) $proof2#254208) (: $fun (-> Cat Weight)))), (let* (((: $proof2#254208 (: $fun (-> Cat Weight))) (synthesize (: $proof2#254208 (: $fun (-> Cat Weight))) kb rb (S (S Z))))) (: (STImplCoer (STTrans (STTrans STRefl STRefl) (STTrans STRefl STRefl)) $proof2#254208) (: $fun (-> Cat Weight)))), (let* (((: $proof2#254208 (: $fun (-> Cat Weight))) (synthesize (: $proof2#254208 (: $fun (-> Cat Weight))) kb rb (S (S Z))))) (: (STImplCoer (STTrans (STTrans STRefl STRefl) (STFnTy STRefl STRefl)) $proof2#254208) (: $fun (-> Cat Weight)))), (let* (((: $proof2#254208 (: $fun (-> Mammal Weight))) (synthesize (: $proof2#254208 (: $fun (-> Mammal Weight))) kb rb (S (S Z))))) (: (STImplCoer (STTrans (STTrans STRefl STRefl) (STFnTy CM STRefl)) $proof2#254208) (: $fun (-> Cat Weight)))), (let* (((: $proof2#254208 (: $fun (-> Cat Weight))) (synthesize (: $proof2#254208 (: $fun (-> Cat Weight))) kb rb (S (S Z))))) (: (STImplCoer (STTrans (STTrans STRefl STRefl) (coerce STRefl STRefl)) $proof2#254208) (: $fun (-> Cat Weight)))), (let* (((: $proof2#254208 (: $fun (-> Cat Weight))) (synthesize (: $proof2#254208 (: $fun (-> Cat Weight))) kb rb (S (S Z))))) (: (STImplCoer (STTrans (STFnTy STRefl STRefl) STRefl) $proof2#254208) (: $fun (-> Cat Weight)))), (let* (((: $proof2#254208 (: $fun (-> Cat Weight))) (synthesize (: $proof2#254208 (: $fun (-> Cat Weight))) kb rb (S (S Z))))) (: (STImplCoer (STTrans (STFnTy STRefl STRefl) (STTrans STRefl STRefl)) $proof2#254208) (: $fun (-> Cat Weight)))), (let* (((: $proof2#254208 (: $fun (-> Cat Weight))) (synthesize (: $proof2#254208 (: $fun (-> Cat Weight))) kb rb (S (S Z))))) (: (STImplCoer (STTrans (STFnTy STRefl STRefl) (STFnTy STRefl STRefl)) $proof2#254208) (: $fun (-> Cat Weight)))), (let* (((: $proof2#254208 (: $fun (-> Mammal Weight))) (synthesize (: $proof2#254208 (: $fun (-> Mammal Weight))) kb rb (S (S Z))))) (: (STImplCoer (STTrans (STFnTy STRefl STRefl) (STFnTy CM STRefl)) $proof2#254208) (: $fun (-> Cat Weight)))), (let* (((: $proof2#254208 (: $fun (-> Cat Weight))) (synthesize (: $proof2#254208 (: $fun (-> Cat Weight))) kb rb (S (S Z))))) (: (STImplCoer (STTrans (STFnTy STRefl STRefl) (coerce STRefl STRefl)) $proof2#254208) (: $fun (-> Cat Weight)))), (let* (((: $proof2#254208 (: $fun (-> Mammal Weight))) (synthesize (: $proof2#254208 (: $fun (-> Mammal Weight))) kb rb (S (S Z))))) (: (STImplCoer (STTrans (STFnTy CM STRefl) STRefl) $proof2#254208) (: $fun (-> Cat Weight)))), (let* (((: $proof2#254208 (: $fun (-> Mammal Weight))) (synthesize (: $proof2#254208 (: $fun (-> Mammal Weight))) kb rb (S (S Z))))) (: (STImplCoer (STTrans (STFnTy CM STRefl) (STTrans STRefl STRefl)) $proof2#254208) (: $fun (-> Cat Weight)))), (let* (((: $proof2#254208 (: $fun (-> Mammal Weight))) (synthesize (: $proof2#254208 (: $fun (-> Mammal Weight))) kb rb (S (S Z))))) (: (STImplCoer (STTrans (STFnTy CM STRefl) (STFnTy STRefl STRefl)) $proof2#254208) (: $fun (-> Cat Weight)))), (let* (((: $proof2#254208 (: $fun (-> Mammal Weight))) (synthesize (: $proof2#254208 (: $fun (-> Mammal Weight))) kb rb (S (S Z))))) (: (STImplCoer (STTrans (STFnTy CM STRefl) (coerce STRefl STRefl)) $proof2#254208) (: $fun (-> Cat Weight)))), (: (STImplCoer (STTrans (STFnTy MA STRefl) (STFnTy CM STRefl)) (STImplCoer (STFnTy AP STRefl) wPW)) (: weigh (-> Cat Weight))), (: (STImplCoer (STTrans (STFnTy MA STRefl) (STFnTy CM STRefl)) (STImplCoer (STFnTy AP STRefl) (STImplCoer STRefl wPW))) (: weigh (-> Cat Weight))), (: (STImplCoer (STTrans (STFnTy MA STRefl) (STFnTy CM STRefl)) (STImplCoer (STFnTy AP STRefl) (coerce STRefl wPW))) (: weigh (-> Cat Weight))), (let* (((: $proof2#254208 (: $fun (-> Cat Weight))) (synthesize (: $proof2#254208 (: $fun (-> Cat Weight))) kb rb (S (S Z))))) (: (STImplCoer (STTrans (coerce STRefl STRefl) STRefl) $proof2#254208) (: $fun (-> Cat Weight)))), (let* (((: $proof2#254208 (: $fun (-> Cat Weight))) (synthesize (: $proof2#254208 (: $fun (-> Cat Weight))) kb rb (S (S Z))))) (: (STImplCoer (STTrans (coerce STRefl STRefl) (STTrans STRefl STRefl)) $proof2#254208) (: $fun (-> Cat Weight)))), (let* (((: $proof2#254208 (: $fun (-> Cat Weight))) (synthesize (: $proof2#254208 (: $fun (-> Cat Weight))) kb rb (S (S Z))))) (: (STImplCoer (STTrans (coerce STRefl STRefl) (STFnTy STRefl STRefl)) $proof2#254208) (: $fun (-> Cat Weight)))), (let* (((: $proof2#254208 (: $fun (-> Mammal Weight))) (synthesize (: $proof2#254208 (: $fun (-> Mammal Weight))) kb rb (S (S Z))))) (: (STImplCoer (STTrans (coerce STRefl STRefl) (STFnTy CM STRefl)) $proof2#254208) (: $fun (-> Cat Weight)))), (let* (((: $proof2#254208 (: $fun (-> Cat Weight))) (synthesize (: $proof2#254208 (: $fun (-> Cat Weight))) kb rb (S (S Z))))) (: (STImplCoer (STTrans (coerce STRefl STRefl) (coerce STRefl STRefl)) $proof2#254208) (: $fun (-> Cat Weight)))), (let* (((: $proof2#254208 (: $fun (-> Cat Weight))) (synthesize (: $proof2#254208 (: $fun (-> Cat Weight))) kb rb (S (S Z))))) (: (STImplCoer (STFnTy STRefl STRefl) $proof2#254208) (: $fun (-> Cat Weight)))), (let* (((: $proof2#254208 (: $fun (-> Cat Weight))) (synthesize (: $proof2#254208 (: $fun (-> Cat Weight))) kb rb (S (S Z))))) (: (STImplCoer (STFnTy STRefl (STTrans STRefl STRefl)) $proof2#254208) (: $fun (-> Cat Weight)))), (let* (((: $proof2#254208 (: $fun (-> Cat Weight))) (synthesize (: $proof2#254208 (: $fun (-> Cat Weight))) kb rb (S (S Z))))) (: (STImplCoer (STFnTy STRefl (coerce STRefl STRefl)) $proof2#254208) (: $fun (-> Cat Weight)))), (let* (((: $proof2#254208 (: $fun (-> Mammal Weight))) (synthesize (: $proof2#254208 (: $fun (-> Mammal Weight))) kb rb (S (S Z))))) (: (STImplCoer (STFnTy CM STRefl) $proof2#254208) (: $fun (-> Cat Weight)))), (let* (((: $proof2#254208 (: $fun (-> Mammal Weight))) (synthesize (: $proof2#254208 (: $fun (-> Mammal Weight))) kb rb (S (S Z))))) (: (STImplCoer (STFnTy CM (STTrans STRefl STRefl)) $proof2#254208) (: $fun (-> Cat Weight)))), (let* (((: $proof2#254208 (: $fun (-> Mammal Weight))) (synthesize (: $proof2#254208 (: $fun (-> Mammal Weight))) kb rb (S (S Z))))) (: (STImplCoer (STFnTy CM (coerce STRefl STRefl)) $proof2#254208) (: $fun (-> Cat Weight)))), (let* (((: $proof2#254208 (: $fun (-> Cat Weight))) (synthesize (: $proof2#254208 (: $fun (-> Cat Weight))) kb rb (S (S Z))))) (: (STImplCoer (STFnTy (STTrans STRefl STRefl) STRefl) $proof2#254208) (: $fun (-> Cat Weight)))), (let* (((: $proof2#254208 (: $fun (-> Cat Weight))) (synthesize (: $proof2#254208 (: $fun (-> Cat Weight))) kb rb (S (S Z))))) (: (STImplCoer (STFnTy (STTrans STRefl STRefl) (STTrans STRefl STRefl)) $proof2#254208) (: $fun (-> Cat Weight)))), (let* (((: $proof2#254208 (: $fun (-> Cat Weight))) (synthesize (: $proof2#254208 (: $fun (-> Cat Weight))) kb rb (S (S Z))))) (: (STImplCoer (STFnTy (STTrans STRefl STRefl) (coerce STRefl STRefl)) $proof2#254208) (: $fun (-> Cat Weight)))), (let* (((: $proof2#254208 (: $fun (-> Mammal Weight))) (synthesize (: $proof2#254208 (: $fun (-> Mammal Weight))) kb rb (S (S Z))))) (: (STImplCoer (STFnTy (STTrans STRefl CM) STRefl) $proof2#254208) (: $fun (-> Cat Weight)))), (let* (((: $proof2#254208 (: $fun (-> Mammal Weight))) (synthesize (: $proof2#254208 (: $fun (-> Mammal Weight))) kb rb (S (S Z))))) (: (STImplCoer (STFnTy (STTrans STRefl CM) (STTrans STRefl STRefl)) $proof2#254208) (: $fun (-> Cat Weight)))), (let* (((: $proof2#254208 (: $fun (-> Mammal Weight))) (synthesize (: $proof2#254208 (: $fun (-> Mammal Weight))) kb rb (S (S Z))))) (: (STImplCoer (STFnTy (STTrans STRefl CM) (coerce STRefl STRefl)) $proof2#254208) (: $fun (-> Cat Weight)))), (let* (((: $proof2#254208 (: $fun (-> Mammal Weight))) (synthesize (: $proof2#254208 (: $fun (-> Mammal Weight))) kb rb (S (S Z))))) (: (STImplCoer (STFnTy (STTrans CM STRefl) STRefl) $proof2#254208) (: $fun (-> Cat Weight)))), (let* (((: $proof2#254208 (: $fun (-> Mammal Weight))) (synthesize (: $proof2#254208 (: $fun (-> Mammal Weight))) kb rb (S (S Z))))) (: (STImplCoer (STFnTy (STTrans CM STRefl) (STTrans STRefl STRefl)) $proof2#254208) (: $fun (-> Cat Weight)))), (let* (((: $proof2#254208 (: $fun (-> Mammal Weight))) (synthesize (: $proof2#254208 (: $fun (-> Mammal Weight))) kb rb (S (S Z))))) (: (STImplCoer (STFnTy (STTrans CM STRefl) (coerce STRefl STRefl)) $proof2#254208) (: $fun (-> Cat Weight)))), (: (STImplCoer (STFnTy (STTrans CM MA) STRefl) (STImplCoer (STFnTy AP STRefl) wPW)) (: weigh (-> Cat Weight))), (: (STImplCoer (STFnTy (STTrans CM MA) STRefl) (STImplCoer (STFnTy AP STRefl) (STImplCoer STRefl wPW))) (: weigh (-> Cat Weight))), (: (STImplCoer (STFnTy (STTrans CM MA) STRefl) (STImplCoer (STFnTy AP STRefl) (coerce STRefl wPW))) (: weigh (-> Cat Weight))), (: (STImplCoer (STFnTy (STTrans CM MA) (STTrans STRefl STRefl)) (STImplCoer (STFnTy AP STRefl) wPW)) (: weigh (-> Cat Weight))), (: (STImplCoer (STFnTy (STTrans CM MA) (STTrans STRefl STRefl)) (STImplCoer (STFnTy AP STRefl) (STImplCoer STRefl wPW))) (: weigh (-> Cat Weight))), (: (STImplCoer (STFnTy (STTrans CM MA) (STTrans STRefl STRefl)) (STImplCoer (STFnTy AP STRefl) (coerce STRefl wPW))) (: weigh (-> Cat Weight))), (: (STImplCoer (STFnTy (STTrans CM MA) (coerce STRefl STRefl)) (STImplCoer (STFnTy AP STRefl) wPW)) (: weigh (-> Cat Weight))), (: (STImplCoer (STFnTy (STTrans CM MA) (coerce STRefl STRefl)) (STImplCoer (STFnTy AP STRefl) (STImplCoer STRefl wPW))) (: weigh (-> Cat Weight))), (: (STImplCoer (STFnTy (STTrans CM MA) (coerce STRefl STRefl)) (STImplCoer (STFnTy AP STRefl) (coerce STRefl wPW))) (: weigh (-> Cat Weight))), (let* (((: $proof2#254208 (: $fun (-> Cat Weight))) (synthesize (: $proof2#254208 (: $fun (-> Cat Weight))) kb rb (S (S Z))))) (: (STImplCoer (STFnTy (coerce STRefl STRefl) STRefl) $proof2#254208) (: $fun (-> Cat Weight)))), (let* (((: $proof2#254208 (: $fun (-> Cat Weight))) (synthesize (: $proof2#254208 (: $fun (-> Cat Weight))) kb rb (S (S Z))))) (: (STImplCoer (STFnTy (coerce STRefl STRefl) (STTrans STRefl STRefl)) $proof2#254208) (: $fun (-> Cat Weight)))), (let* (((: $proof2#254208 (: $fun (-> Cat Weight))) (synthesize (: $proof2#254208 (: $fun (-> Cat Weight))) kb rb (S (S Z))))) (: (STImplCoer (STFnTy (coerce STRefl STRefl) (coerce STRefl STRefl)) $proof2#254208) (: $fun (-> Cat Weight)))), (let* (((: $proof2#254208 (: $fun (-> Mammal Weight))) (synthesize (: $proof2#254208 (: $fun (-> Mammal Weight))) kb rb (S (S Z))))) (: (STImplCoer (STFnTy (coerce STRefl CM) STRefl) $proof2#254208) (: $fun (-> Cat Weight)))), (let* (((: $proof2#254208 (: $fun (-> Mammal Weight))) (synthesize (: $proof2#254208 (: $fun (-> Mammal Weight))) kb rb (S (S Z))))) (: (STImplCoer (STFnTy (coerce STRefl CM) (STTrans STRefl STRefl)) $proof2#254208) (: $fun (-> Cat Weight)))), (let* (((: $proof2#254208 (: $fun (-> Mammal Weight))) (synthesize (: $proof2#254208 (: $fun (-> Mammal Weight))) kb rb (S (S Z))))) (: (STImplCoer (STFnTy (coerce STRefl CM) (coerce STRefl STRefl)) $proof2#254208) (: $fun (-> Cat Weight)))), (let* (((: $proof2#254208 (: $fun (-> Cat Weight))) (synthesize (: $proof2#254208 (: $fun (-> Cat Weight))) kb rb (S (S Z))))) (: (STImplCoer (coerce STRefl STRefl) $proof2#254208) (: $fun (-> Cat Weight)))), (let* (((: $proof2#254208 (: $fun (-> Cat Weight))) (synthesize (: $proof2#254208 (: $fun (-> Cat Weight))) kb rb (S (S Z))))) (: (STImplCoer (coerce STRefl (STTrans STRefl STRefl)) $proof2#254208) (: $fun (-> Cat Weight)))), (let* (((: $proof2#254208 (: $fun (-> Cat Weight))) (synthesize (: $proof2#254208 (: $fun (-> Cat Weight))) kb rb (S (S Z))))) (: (STImplCoer (coerce STRefl (STFnTy STRefl STRefl)) $proof2#254208) (: $fun (-> Cat Weight)))), (let* (((: $proof2#254208 (: $fun (-> Mammal Weight))) (synthesize (: $proof2#254208 (: $fun (-> Mammal Weight))) kb rb (S (S Z))))) (: (STImplCoer (coerce STRefl (STFnTy CM STRefl)) $proof2#254208) (: $fun (-> Cat Weight)))), (let* (((: $proof2#254208 (: $fun (-> Cat Weight))) (synthesize (: $proof2#254208 (: $fun (-> Cat Weight))) kb rb (S (S Z))))) (: (STImplCoer (coerce STRefl (coerce STRefl STRefl)) $proof2#254208) (: $fun (-> Cat Weight)))), (let* (((: $proof2#254208 (: $fun (-> Cat Weight))) (synthesize (: $proof2#254208 (: $fun (-> Cat Weight))) kb rb (S (S Z))))) (: (STImplCoer (coerce (STTrans STRefl STRefl) STRefl) $proof2#254208) (: $fun (-> Cat Weight)))), (let* (((: $proof2#254208 (: $fun (-> Cat Weight))) (synthesize (: $proof2#254208 (: $fun (-> Cat Weight))) kb rb (S (S Z))))) (: (STImplCoer (coerce (STTrans STRefl STRefl) (STTrans STRefl STRefl)) $proof2#254208) (: $fun (-> Cat Weight)))), (let* (((: $proof2#254208 (: $fun (-> Cat Weight))) (synthesize (: $proof2#254208 (: $fun (-> Cat Weight))) kb rb (S (S Z))))) (: (STImplCoer (coerce (STTrans STRefl STRefl) (STFnTy STRefl STRefl)) $proof2#254208) (: $fun (-> Cat Weight)))), (let* (((: $proof2#254208 (: $fun (-> Mammal Weight))) (synthesize (: $proof2#254208 (: $fun (-> Mammal Weight))) kb rb (S (S Z))))) (: (STImplCoer (coerce (STTrans STRefl STRefl) (STFnTy CM STRefl)) $proof2#254208) (: $fun (-> Cat Weight)))), (let* (((: $proof2#254208 (: $fun (-> Cat Weight))) (synthesize (: $proof2#254208 (: $fun (-> Cat Weight))) kb rb (S (S Z))))) (: (STImplCoer (coerce (STTrans STRefl STRefl) (coerce STRefl STRefl)) $proof2#254208) (: $fun (-> Cat Weight)))), (let* (((: $proof2#254208 (: $fun (-> Cat Weight))) (synthesize (: $proof2#254208 (: $fun (-> Cat Weight))) kb rb (S (S Z))))) (: (STImplCoer (coerce (coerce STRefl STRefl) STRefl) $proof2#254208) (: $fun (-> Cat Weight)))), (let* (((: $proof2#254208 (: $fun (-> Cat Weight))) (synthesize (: $proof2#254208 (: $fun (-> Cat Weight))) kb rb (S (S Z))))) (: (STImplCoer (coerce (coerce STRefl STRefl) (STTrans STRefl STRefl)) $proof2#254208) (: $fun (-> Cat Weight)))), (let* (((: $proof2#254208 (: $fun (-> Cat Weight))) (synthesize (: $proof2#254208 (: $fun (-> Cat Weight))) kb rb (S (S Z))))) (: (STImplCoer (coerce (coerce STRefl STRefl) (STFnTy STRefl STRefl)) $proof2#254208) (: $fun (-> Cat Weight)))), (let* (((: $proof2#254208 (: $fun (-> Mammal Weight))) (synthesize (: $proof2#254208 (: $fun (-> Mammal Weight))) kb rb (S (S Z))))) (: (STImplCoer (coerce (coerce STRefl STRefl) (STFnTy CM STRefl)) $proof2#254208) (: $fun (-> Cat Weight)))), (let* (((: $proof2#254208 (: $fun (-> Cat Weight))) (synthesize (: $proof2#254208 (: $fun (-> Cat Weight))) kb rb (S (S Z))))) (: (STImplCoer (coerce (coerce STRefl STRefl) (coerce STRefl STRefl)) $proof2#254208) (: $fun (-> Cat Weight)))), (let* (((: $proof2#338763 (: $fun#338926 (-> Cat Weight))) (synthesize (: $proof2#338763 (: $fun#338926 (-> Cat Weight))) kb rb (S (S Z))))) (: (coerce STRefl $proof2#338763) (: $fun#338926 (-> Cat Weight)))), (let* (((: $proof2#338763 (: $fun#342712 (-> Cat Weight))) (synthesize (: $proof2#338763 (: $fun#342712 (-> Cat Weight))) kb rb (S (S Z))))) (: (coerce (STTrans STRefl STRefl) $proof2#338763) (: $fun#342712 (-> Cat Weight)))), (let* (((: $proof2#338763 (: $fun#343216 (-> Cat Weight))) (synthesize (: $proof2#338763 (: $fun#343216 (-> Cat Weight))) kb rb (S (S Z))))) (: (coerce (STTrans STRefl (STTrans STRefl STRefl)) $proof2#338763) (: $fun#343216 (-> Cat Weight)))), (let* (((: $proof2#338763 (: $fun#344079 (-> Cat Weight))) (synthesize (: $proof2#338763 (: $fun#344079 (-> Cat Weight))) kb rb (S (S Z))))) (: (coerce (STTrans STRefl (coerce STRefl STRefl)) $proof2#338763) (: $fun#344079 (-> Cat Weight)))), (let* (((: $proof2#338763 (: $fun#348143 (-> Cat Weight))) (synthesize (: $proof2#338763 (: $fun#348143 (-> Cat Weight))) kb rb (S (S Z))))) (: (coerce (STTrans (STTrans STRefl STRefl) STRefl) $proof2#338763) (: $fun#348143 (-> Cat Weight)))), (let* (((: $proof2#338763 (: $fun#348647 (-> Cat Weight))) (synthesize (: $proof2#338763 (: $fun#348647 (-> Cat Weight))) kb rb (S (S Z))))) (: (coerce (STTrans (STTrans STRefl STRefl) (STTrans STRefl STRefl)) $proof2#338763) (: $fun#348647 (-> Cat Weight)))), (let* (((: $proof2#338763 (: $fun#349510 (-> Cat Weight))) (synthesize (: $proof2#338763 (: $fun#349510 (-> Cat Weight))) kb rb (S (S Z))))) (: (coerce (STTrans (STTrans STRefl STRefl) (coerce STRefl STRefl)) $proof2#338763) (: $fun#349510 (-> Cat Weight)))), (let* (((: $proof2#338763 (: $fun#369954 (-> Cat Weight))) (synthesize (: $proof2#338763 (: $fun#369954 (-> Cat Weight))) kb rb (S (S Z))))) (: (coerce (STTrans (coerce STRefl STRefl) STRefl) $proof2#338763) (: $fun#369954 (-> Cat Weight)))), (let* (((: $proof2#338763 (: $fun#370458 (-> Cat Weight))) (synthesize (: $proof2#338763 (: $fun#370458 (-> Cat Weight))) kb rb (S (S Z))))) (: (coerce (STTrans (coerce STRefl STRefl) (STTrans STRefl STRefl)) $proof2#338763) (: $fun#370458 (-> Cat Weight)))), (let* (((: $proof2#338763 (: $fun#371321 (-> Cat Weight))) (synthesize (: $proof2#338763 (: $fun#371321 (-> Cat Weight))) kb rb (S (S Z))))) (: (coerce (STTrans (coerce STRefl STRefl) (coerce STRefl STRefl)) $proof2#338763) (: $fun#371321 (-> Cat Weight)))), (let* (((: $proof2#338763 (: $fun#374352 (-> Cat Weight))) (synthesize (: $proof2#338763 (: $fun#374352 (-> Cat Weight))) kb rb (S (S Z))))) (: (coerce (coerce STRefl STRefl) $proof2#338763) (: $fun#374352 (-> Cat Weight)))), (let* (((: $proof2#338763 (: $fun#374856 (-> Cat Weight))) (synthesize (: $proof2#338763 (: $fun#374856 (-> Cat Weight))) kb rb (S (S Z))))) (: (coerce (coerce STRefl (STTrans STRefl STRefl)) $proof2#338763) (: $fun#374856 (-> Cat Weight)))), (let* (((: $proof2#338763 (: $fun#375734 (-> Cat Weight))) (synthesize (: $proof2#338763 (: $fun#375734 (-> Cat Weight))) kb rb (S (S Z))))) (: (coerce (coerce STRefl (coerce STRefl STRefl)) $proof2#338763) (: $fun#375734 (-> Cat Weight)))), (let* (((: $proof2#338763 (: $fun#376370 (-> Cat Weight))) (synthesize (: $proof2#338763 (: $fun#376370 (-> Cat Weight))) kb rb (S (S Z))))) (: (coerce (coerce (STTrans STRefl STRefl) STRefl) $proof2#338763) (: $fun#376370 (-> Cat Weight)))), (let* (((: $proof2#338763 (: $fun#376874 (-> Cat Weight))) (synthesize (: $proof2#338763 (: $fun#376874 (-> Cat Weight))) kb rb (S (S Z))))) (: (coerce (coerce (STTrans STRefl STRefl) (STTrans STRefl STRefl)) $proof2#338763) (: $fun#376874 (-> Cat Weight)))), (let* (((: $proof2#338763 (: $fun#377752 (-> Cat Weight))) (synthesize (: $proof2#338763 (: $fun#377752 (-> Cat Weight))) kb rb (S (S Z))))) (: (coerce (coerce (STTrans STRefl STRefl) (coerce STRefl STRefl)) $proof2#338763) (: $fun#377752 (-> Cat Weight)))), (let* (((: $proof2#338763 (: $fun#378427 (-> Cat Weight))) (synthesize (: $proof2#338763 (: $fun#378427 (-> Cat Weight))) kb rb (S (S Z))))) (: (coerce (coerce (coerce STRefl STRefl) STRefl) $proof2#338763) (: $fun#378427 (-> Cat Weight)))), (let* (((: $proof2#338763 (: $fun#378931 (-> Cat Weight))) (synthesize (: $proof2#338763 (: $fun#378931 (-> Cat Weight))) kb rb (S (S Z))))) (: (coerce (coerce (coerce STRefl STRefl) (STTrans STRefl STRefl)) $proof2#338763) (: $fun#378931 (-> Cat Weight)))), (let* (((: $proof2#338763 (: $fun#379809 (-> Cat Weight))) (synthesize (: $proof2#338763 (: $fun#379809 (-> Cat Weight))) kb rb (S (S Z))))) (: (coerce (coerce (coerce STRefl STRefl) (coerce STRefl STRefl)) $proof2#338763) (: $fun#379809 (-> Cat Weight))))]