proposition: Lemma CorrectEncoder_Union {m} (formats : Vector.t (FormatM S T) m) (encoders : Vector.t (EncodeM S T) m) (correct_encoders : Iterate_Ensemble_BoundedIndex' (fun idx => CorrectEncoder (Vector.nth formats idx) (Vector.nth encoders idx))) (f_idx : forall (s : S), { idx : _ & forall env t env', Union_Format formats s env ∋ (t, env') -> Vector.nth formats idx s env ∋ (t, env')}) : CorrectEncoder (Union_Format formats) (Union_Encode encoders (fun s => projT1 (f_idx s))).
proof: Proof. unfold CorrectEncoder, Union_Encode, Union_Format in *; split; intros. - apply Iterate_Ensemble_equiv' with (idx := projT1 (f_idx a)) in correct_encoders. eapply correct_encoders in H. apply unfold_computes; eauto. - intro; apply_in_hyp @unfold_computes; eauto. pose proof (projT2 (f_idx a) env _ _ H0); simpl in *. apply Iterate_Ensemble_equiv' with (idx := projT1 (f_idx a)) in correct_encoders. eapply correct_encoders in H. apply H; eauto. Qed.
imports: Fiat.Common.ilist Fiat.Common.IterateBoundedIndex Fiat.Narcissus.Common.Specs Coq.Sets.Ensembles