cf cg : Code
this : ?m.357933
⊢ encode cf < encode (comp cf cg) ∧ encode cg < encode (comp cf cg)

case this
cf cg : Code
⊢ ?m.357933
cf cg : Code
⊢ encode cf < encode (comp cf cg) ∧ encode cg < encode (comp cf cg)
suffices
case this
cf cg : Code
⊢ encode (pair cf cg) < encode (comp cf cg)
cf cg : Code
this : ?m.357933
⊢ encode cf < encode (comp cf cg) ∧ encode cg < encode (comp cf cg)

case this
cf cg : Code
⊢ ?m.357933
exact (encode_lt_pair cf cg).imp (fun h => lt_trans h this) fun h => lt_trans h this
case this
cf cg : Code
⊢ encode (pair cf cg) < encode (comp cf cg)
case this
cf cg : Code
⊢ encode (pair cf cg) < encode (comp cf cg)
change _
no goals
case this
cf cg : Code
⊢ encode (pair cf cg) < encode (comp cf cg)
simp [encodeCode_eq, encodeCode]