+lemma compl_g6: ∀h.
+ constructible (λx. h (fst x) (snd x)) →
+ (CF (λx. sU 〈max (fst (snd x)) (snd (snd x)),〈fst x,h (S (fst (snd x))) (fst x)〉〉)
+ (λp.termb (fst (snd p)) (fst p) (h (S (fst (snd p))) (fst p)))).
+#h #hconstr @(ext_CF (termb_aux h))
+ [#n normalize >fst_pair >snd_pair >fst_pair >snd_pair // ]
+@(CF_comp … (λx.MSC x + h (S (fst (snd x))) (fst x)) … CF_termb)
+ [@CF_comp_pair
+ [@CF_comp_fst @(monotonic_CF … CF_snd) #x //
+ |@CF_comp_pair
+ [@(monotonic_CF … CF_fst) #x //
+ |@(ext_CF ((λx.h (fst x) (snd x))∘(λx.〈S (fst (snd x)),fst x〉)))
+ [#n normalize >fst_pair >snd_pair %]
+ @(CF_comp … MSC …hconstr)
+ [@CF_comp_pair [@CF_compS @CF_comp_fst // |//]
+ |@O_plus @le_to_O [//|#n >fst_pair >snd_pair //]
+ ]
+ ]
+ ]
+ |@O_plus
+ [@O_plus
+ [@(O_trans … (λx.MSC (fst x) + MSC (max (fst (snd x)) (snd (snd x)))))
+ [%{2} %{0} #x #_ cases (surj_pair x) #a * #b #eqx >eqx
+ >fst_pair >snd_pair @(transitive_le … (MSC_pair …))
+ >distributive_times_plus @le_plus [//]
+ cases (surj_pair b) #c * #d #eqb >eqb
+ >fst_pair >snd_pair @(transitive_le … (MSC_pair …))
+ whd in ⊢ (??%); @le_plus
+ [@monotonic_MSC @(le_maxl … (le_n …))
+ |>commutative_times <times_n_1 @monotonic_MSC @(le_maxr … (le_n …))
+ ]
+ |@O_plus [@le_to_O #x @sU_le_x |@le_to_O #x @sU_le_i]
+ ]
+ |@le_to_O #n @sU_le
+ ]
+ |@le_to_O #x @monotonic_sU // @(le_maxl … (le_n …)) ]
+ ]
+qed.
+
+(* definition faux1 ≝ λh.