proposition: Lemma wrespect5_companion clo (RES: wrespectful5 clo): clo <6= cpn5 gf.
proof: Proof. intros. eapply wrespect5_compatible' in RES. eapply (@compatible'5_companion (rclo5 clo)) in RES; [apply RES|]. eapply rclo5_clo_base, PR. Qed.
imports: Program.Basics Paco(paco5 pacotac)