(*** at_ext *)
corec theorem pr_eq_ext_pat (f1) (f2): ðâšf1â© â ðâšf2â© â
(âi,i1,i2. @âši,f1â© â i1 â @âši,f2â© â i2 â i1 = i2) â
(*** at_ext *)
corec theorem pr_eq_ext_pat (f1) (f2): ðâšf1â© â ðâšf2â© â
(âi,i1,i2. @âši,f1â© â i1 â @âši,f2â© â i2 â i1 = i2) â